Support zero-arity constructors (constants)

[hritcu]

Committed a first attempt to fix this. Needs some testing.

[hritcu]

This works on all old examples (without nullary constructors).

However, it doesn't work on polymorphic nullary constructors. Inference seems impossible in this case. Indeed, alg_constr in typeterm.ml raises an exception: "result type for alg_constr is not ground".

alg_constr m f = match m with

| Constr(m',_) ->

let tl, t = get_types_f m' in if List.length tl = 0 && not(well_formed f) then

(Logmanager.log "gamma:$e\n" ~environment:[f] ~loglevel:3; raise (Termtyping "zeroary constructor and gamma not well formed"))

else

let t'l = compute_input_types_f m' f in let sigma = unify t'l tl f in let result_t = apply sigma t in if is_ground result_t then

result_t

else (* XXX zeroary sufficiently solved? *)

raise (Termtyping "result type for alg_constr is not ground")

| _ -> raise (Invalid_argument "typeterm.ml(alg_constr): no constructor given")

[hritcu]

Previous code snipped got fucked up. Here is goes again:

alg_constr m f = match m with
	| Constr(m',_) ->					
		let tl, t = get_types_f m' in
		if List.length tl = 0 && not(well_formed f) then
			(Logmanager.log "gamma:$e\n" ~environment:[f] ~loglevel:3;
			raise (Termtyping "zeroary constructor and gamma not well formed"))
		else
			let t'l = compute_input_types_f m' f in
			let sigma = unify t'l tl f in
			let result_t = apply sigma t in
			if is_ground result_t then 
				result_t 
			else		(* XXX zeroary sufficiently solved? *)
				raise (Termtyping "result type for alg_constr is not ground")
	| _ -> raise (Invalid_argument "typeterm.ml(alg_constr): no constructor given")

[hritcu]

Allowing the user to annotate polymorphic nullary constructors.

Looks like this: let emptylist = nil()(*:List(Un)*) in 0

[hritcu]

Missed one fix in spassprint.ml, it's in now.