Ticket #100 (closed feature: fixed)

Opened 5 years ago

Last modified 5 years ago

Support zero-arity constructors (constants)

Reported by: hritcu Owned by: hritcu
Priority: major Milestone: 0.2.1
Component: zk-typechecker Keywords:
Cc:

Description


Change History

comment:1 Changed 5 years ago by hritcu

  • Owner changed from somebody to hritcu

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

comment:2 Changed 5 years ago by 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")

comment:3 Changed 5 years ago by 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")

comment:4 Changed 5 years ago by hritcu

  • Status changed from new to closed
  • Resolution set to fixed

Allowing the user to annotate polymorphic nullary constructors.

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

comment:5 Changed 5 years ago by hritcu

  • Status changed from closed to reopened
  • Resolution fixed deleted

comment:6 Changed 5 years ago by hritcu

  • Status changed from reopened to closed
  • Resolution set to fixed

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

Note: See TracTickets for help on using tickets.