finaly passed the first examples

TODO

@@ -1,14 +1,11 @@
 (* calculus_misc should populate himself during the process *)
 0) pprinter / parser
-   + test1.p passed line by line in regression
-   - Enhanced
 1) calculus_substitution
-   - need to be tested
 2) reduction
-   - need to be tested
 3) unification
-   - add match
+   - need to add flushing of terms 
+   - higher order unification
 4) terminfer
    - add using conversion when not solvable
 5) termcheck
-   - add final implicit
+

src/core/kernel/calculus_def.ml

@@ -81,6 +81,7 @@ and pattern = PAvar | PName of string
 
 and typeannotation = NoAnnotation
 		     | Annotation of term
+		     | TypedAnnotation of term
 		     | Typed of term
 
 
@@ -129,6 +130,7 @@ type poussin_error = FreeError of string
 		    | NegativeIndexBVar of int
 		    | UnknownBVar of context * int
 		    | UnknownFVar of context * int
+		    | NotInductiveDestruction of context * term
 
 
 exception PoussinException of poussin_error

src/core/kernel/calculus_misc.ml

@@ -32,6 +32,9 @@ let lambda_ ?(annot: typeannotation = NoAnnotation) ?(posq: position = NoPositio
 let forall_ ?(annot: typeannotation = NoAnnotation) ?(posq: position = NoPosition) ?(posl: position = NoPosition) (name: name) ?(nature: nature = Explicit) ?(ty: term = avar_ ()) (body: term) : term =
   Forall ((name, ty, nature, posl), body, annot, posl, false)
 
+let app_ ?(annot: typeannotation = NoAnnotation) ?(pos: position = NoPosition) f args =
+  App (f, args, annot, pos, false)
+
 (* function for deconstructing/constructing contiguous lambdas *)
 let rec destruct_lambda (te: term) : ((name * term * nature * position) * typeannotation * position) list * term =
   match te with
@@ -82,6 +85,29 @@ let set_term_annotation (te: term) (ty: term) : term =
     | Match (te, des, _, pos, reduced) ->
       Match (te, des, Annotation ty, pos, reduced)
 
+let set_term_tannotation (te: term) (ty: term) : term =
+  match te with
+    | Universe (ty, lvl, pos) -> 
+      Universe (ty, lvl, pos)
+    | Cste (n, _, pos, reduced) ->
+      Cste (n, TypedAnnotation ty, pos, reduced)
+    | Var (i, _, pos) ->
+      Var (i, TypedAnnotation ty, pos)
+    | AVar (_, pos) ->
+      AVar (TypedAnnotation ty, pos)
+    | TName (n, _, pos) ->
+      TName (n, TypedAnnotation ty, pos)
+    | Lambda (q, te, _, pos, reduced) ->
+      Lambda (q, te, TypedAnnotation ty, pos, reduced)
+    | Forall (q, te, _, pos, reduced) ->
+      Forall (q, te, TypedAnnotation ty, pos, reduced)
+    | Let (q, te, _, pos, reduced) ->
+      Let (q, te, TypedAnnotation ty, pos, reduced)
+    | App (f, args, _, pos, reduced) ->
+      App (f, args, TypedAnnotation ty, pos, reduced)
+    | Match (te, des, _, pos, reduced) ->
+      Match (te, des, TypedAnnotation ty, pos, reduced)
+
 let set_term_type (te: term) (ty: term) : term =
   match te with
     | Universe (ty, lvl, pos) -> 
@@ -150,6 +176,7 @@ and fv_typeannotation (ty: typeannotation) : IndexSet.t =
   match ty with
     | NoAnnotation -> IndexSet.empty
     | Annotation te -> fv_term te
+    | TypedAnnotation te -> fv_term te
     | Typed te -> fv_term te
 
 
@@ -212,6 +239,7 @@ and bv_typeannotation (ty: typeannotation) : IndexSet.t =
   match ty with
     | NoAnnotation -> IndexSet.empty
     | Annotation te -> bv_term te
+    | TypedAnnotation te -> bv_term te
     | Typed te -> bv_term te
 
 

src/core/kernel/calculus_parser.ml

@@ -436,7 +436,7 @@ let rec parse_definition (defs: defs) (leftmost: int * int) : definition parsing
     DefDefinition (s, 
 		  (set_term_annotation 
 		     (set_term_pos 
-			(build_lambdas qs te) 
+			(build_lambdas qs (set_term_annotation te ty)) 
 			(pos_to_position (startpos2, endpos2))
 		     )
 		     (set_term_pos 

src/core/kernel/calculus_pprinter.ml

@@ -23,18 +23,46 @@ type pp_option = {
   show_indices : bool;
   show_position : bool;
   show_univ : bool;
+  show_type: bool;
 }
 
 let pp_option = ref {show_implicit = true; 
 		     show_indices = true; 
 		     show_position = false; 
 		     show_univ = false;
+		     show_type = false;
 		    }
 
 let verbatims (l: name list) = Verbatim (String.concat "" l)
 
 (* transform a term into a box *)
 let rec term2token (vars: name list) (te: term) (p: place): token =
+  match get_term_annotation te with 
+    | Typed ty when !pp_option.show_type ->
+      Box [Verbatim "(";
+	   term2token vars (set_term_noannotation te) Alone; Space 1;
+	   Verbatim "::"; Space 1;
+	   term2token vars ty Alone;
+	   Verbatim ")"
+	  ]
+
+    | Annotation ty when !pp_option.show_type ->
+      Box [Verbatim "(";
+	   term2token vars (set_term_noannotation te) Alone; Space 1;
+	   Verbatim ":?:"; Space 1;
+	   term2token vars ty Alone;
+	   Verbatim ")"
+	  ]
+
+    | TypedAnnotation ty when !pp_option.show_type ->
+      Box [Verbatim "(";
+	   term2token vars (set_term_noannotation te) Alone; Space 1;
+	   Verbatim ":?:"; Space 1;
+	   term2token vars ty Alone;
+	   Verbatim ")"
+	  ]
+
+    | _ ->
   match te with
 
     | Universe (Type, _, _) -> Verbatim "Type"
@@ -252,7 +280,7 @@ let substitution2string (ctxt: context ref) (s: substitution) : string =
 
 let poussin_error2token (err: poussin_error) : token =
   match err with
-    | FreeError s -> Verbatim "FreeError"
+    | FreeError s -> Verbatim s
     | Unshiftable_term _ -> Verbatim "Unshiftable_term"
     | UnknownCste s -> verbatims ["UnknownCste: "; s]
     | NoUnification (ctxt, te1, te2) -> 
@@ -261,10 +289,14 @@ let poussin_error2token (err: poussin_error) : token =
 	   term2token (context2namelist (ref ctxt)) te2 Alone; Newline]
 
     | NoNatureUnification  _ -> Verbatim "NoNatureUnification"
-    | UnknownUnification  _ -> Verbatim "UnknownUnification"
+    | UnknownUnification (ctxt, te1, te2) -> 
+      Box [Verbatim "UnknownUnification between"; Newline; 
+	   term2token (context2namelist (ref ctxt)) te1 Alone; Newline; 
+	   term2token (context2namelist (ref ctxt)) te2 Alone; Newline]
     | NegativeIndexBVar  _ -> Verbatim "NegativeIndexBVar"
     | UnknownBVar  _ -> Verbatim "UnknownBVar"
     | UnknownFVar _ -> Verbatim "UnknownFVar"
+    | NotInductiveDestruction _ -> Verbatim "NotInductiveDestruction"
 
 let poussin_error2string (err: poussin_error) : string =
   let token = poussin_error2token err in

src/core/kernel/calculus_reduction.ml

@@ -57,108 +57,104 @@ let rec pattern_match (p: pattern) (te: term) : (term list) option =
 *)
 
 let rec reduction_term (defs: defs) (strat: reduction_strategy) (te: term) : term = 
-  match te with
-    | Universe _ | Var _ | AVar _ | TName _ -> te
-
-    | _ when is_reduced te -> te
-
-    | Cste (n, ty, position, _) -> (
-      match strat.delta with
-	(* no unfolding *)
-	| None -> te
-
-	| Some delta -> (
-	  try 
-	    match Hashtbl.find defs n with
-	      (* delta strong -> we return it 
-		 delta_weak -> we make sure the resulting term is 'clean'
-	      *)
-	      | Definition te ->
-		let te' = reduction_term defs strat te in
-		set_reduced (
-		  match delta with
-		    | DeltaStrong -> te'
-		    | DeltaWeak when is_clean_term te' -> te'
-		    | _ -> te
-		)
-	      | _ -> set_reduced te
-	  with
-	    | Not_found -> raise (PoussinException (UnknownCste n))
-
-	)
-
-    )
-
-    | Lambda _ | Forall _ when strat.beta != Some BetaStrong -> set_reduced te
-
-    | Lambda ((n, ty, nature, pos), te, ty2, pos2, _) ->
-      (
-	let te = reduction_term defs strat te in
-	Lambda ((n, ty, nature, pos), te, ty2, pos2, true)
+  let te' = (
+    match te with
+      | Universe _ | Var _ | AVar _ | TName _ -> te
+
+      | _ when is_reduced te -> te
+
+      | Cste (n, ty, position, _) -> (
+	try 
+	  match Hashtbl.find defs n with
+		(* delta strong -> we return it 
+		   delta_weak -> we make sure the resulting term is 'clean'
+		*)
+	    | Definition te -> (
+	      match strat.delta with
+		| Some _ -> 
+		  let te' = reduction_term defs strat te in
+		  te'
+		| None -> set_reduced te
+	    )
+	    | _ -> set_reduced te
+	with
+	  | Not_found -> raise (PoussinException (UnknownCste n))
+
       )
+
+      | Lambda _ | Forall _ when strat.beta != Some BetaStrong -> set_reduced te
 
-    | Forall ((n, ty, nature, pos), te, ty2, pos2, _) ->
-      (
-	let te = reduction_term defs strat te in
-	Forall ((n, ty, nature, pos), te, ty2, pos2, true)
-      )
+      | Lambda ((n, ty, nature, pos), te, ty2, pos2, _) ->
+	(
+	  let te = reduction_term defs strat te in
+	  Lambda ((n, ty, nature, pos), te, ty2, pos2, true)
+	)
 
-    | Let _ when strat.zeta = false && strat.beta != Some BetaStrong -> set_reduced te
-    | Let ((n, te, pos), te2, ty, pos2, _) when strat.zeta = false && strat.beta = Some BetaStrong ->
-      Let ((n, te, pos), reduction_term defs strat te2, ty, pos2, true)
+      | Forall ((n, ty, nature, pos), te, ty2, pos2, _) ->
+	(
+	  let te = reduction_term defs strat te in
+	  Forall ((n, ty, nature, pos), te, ty2, pos2, true)
+	)
 
-    | Let ((n, te, pos), te2, ty, pos2, _) when strat.zeta = true ->
+      | Let _ when strat.zeta = false && strat.beta != Some BetaStrong -> set_reduced te
+      | Let ((n, te, pos), te2, ty, pos2, _) when strat.zeta = false && strat.beta = Some BetaStrong ->
+	Let ((n, te, pos), reduction_term defs strat te2, ty, pos2, true)
+
+      | Let ((n, te, pos), te2, ty, pos2, _) when strat.zeta = true ->
       (* here we compute the reduction of te and shift it such that it is at the same level as te2 *)
-      let te = shift_term (reduction_term defs strat te) 1 in
+	let te = shift_term (reduction_term defs strat te) 1 in
       (* we substitute all occurence of n by te *)
-      let te2 = term_substitution (IndexMap.singleton 0 te) te2 in
+	let te2 = term_substitution (IndexMap.singleton 0 te) te2 in
       (* and we shift back to the proper level *)
-      let te2 = shift_term te2 (-1) in
-      reduction_term defs strat te2
-
-    | Match _ when strat.iota = false -> set_reduced te
-    | Match (dte, des, ty, pos, _) -> (
-      let dte = reduction_term defs strat dte in
-      let res = fold_stop (fun () (ps, body) ->
-	fold_stop (fun () p ->
-	  match pattern_match p dte with
-	    | None -> Left ()
-	    | Some l ->
+	let te2 = shift_term te2 (-1) in
+	reduction_term defs strat te2
+
+      | Match _ when strat.iota = false -> set_reduced te
+      | Match (dte, des, ty, pos, _) -> (
+	let dte = reduction_term defs strat dte in
+	let res = fold_stop (fun () (ps, body) ->
+	  fold_stop (fun () p ->
+	    match pattern_match p dte with
+	      | None -> Left ()
+	      | Some l ->
 	      (* we will do the same thing as in let, but on the reversed order of the matching list *)
-	      let te = List.fold_left (fun acc te -> 
+		let te = List.fold_left (fun acc te -> 
 		(* rewrite the var 0 *)
-		let acc = term_substitution (IndexMap.singleton 0 te) acc in
+		  let acc = term_substitution (IndexMap.singleton 0 te) acc in
 		(* shift the term by -1 *)
-		let acc = shift_term acc (-1) in
-		acc
-	      ) 
-		body 
-		(List.map (fun te -> shift_term te (List.length l)) (List.rev l)) in
-	      Right te
-	) () ps
-      ) () des in
-      match res with
-	| Left () -> set_reduced te
-	| Right te -> reduction_term defs strat te
-    )
-
-    | App (Lambda ((n, ty, nature, pos), te, ty2, pos2, _), (hd1, hd2)::tl, app_ty, app_pos, _) ->
-      let hd1 = shift_term (reduction_term defs strat hd1) 1 in
-      let f = term_substitution (IndexMap.singleton 0 hd1) te in
-      reduction_term defs strat (App (shift_term f (-1), tl, app_ty, app_pos, false))
-
-    | App (f, [], _, _, _) ->
-      set_reduced (reduction_term defs strat f)
-
-    | App (f, args, ty, pos, _) when not (is_reduced f) -> (
-      let f = reduction_term defs strat f in
-      set_reduced (reduction_term defs strat (App (f, args, ty, pos, false)))
-    )
-
-    | App (f, args, ty, pos, _) when is_reduced f ->
-      let args = List.map (fun (te, n) -> reduction_term defs strat te, n) args in
-      App (f, args, ty, pos, true)
+		  let acc = shift_term acc (-1) in
+		  acc
+		) 
+		  body 
+		  (List.map (fun te -> shift_term te (List.length l)) (List.rev l)) in
+		Right te
+	  ) () ps
+	) () des in
+	match res with
+	  | Left () -> set_reduced te
+	  | Right te -> reduction_term defs strat te
+      )
+
+      | App (Lambda ((n, ty, nature, pos), te, ty2, pos2, _), (hd1, hd2)::tl, app_ty, app_pos, _) ->
+	let hd1 = shift_term (reduction_term defs strat hd1) 1 in
+	let f = term_substitution (IndexMap.singleton 0 hd1) te in
+	reduction_term defs strat (App (shift_term f (-1), tl, app_ty, app_pos, false))
+
+      | App (f, [], _, _, _) ->
+	set_reduced (reduction_term defs strat f)
+
+      | App (f, args, ty, pos, _) when not (is_reduced f) -> (
+	let f = reduction_term defs strat f in
+	set_reduced (reduction_term defs strat (App (f, args, ty, pos, false)))
+      )
 
+      | App (f, args, ty, pos, _) when is_reduced f ->
+	let args = List.map (fun (te, n) -> reduction_term defs strat te, n) args in
+	App (f, args, ty, pos, true)
+  ) in
+  match strat.delta with
+    | Some DeltaWeak when is_clean_term te' -> te'
+    | _ -> set_reduced te      
 
 
 and reduction_typeannotation (defs: defs) (strat: reduction_strategy) (ty: typeannotation) : typeannotation =

src/core/kernel/calculus_substitution.ml

@@ -64,7 +64,9 @@ and leveled_shift_term (te: term) (level: int) (delta: int) : term =
 and leveled_shift_typeannotation (ty: typeannotation) (level: int) (delta: int) : typeannotation =
   match ty with
     | NoAnnotation -> NoAnnotation
+      (* this case should be an error ... *)
     | Annotation te -> Annotation (leveled_shift_term te level delta)
+    | TypedAnnotation te -> TypedAnnotation (leveled_shift_term te level delta)
     | Typed te -> Typed (leveled_shift_term te level delta)
 
 and leveled_shift_destructor (des: pattern list * term) (level: int) (delta: int) : pattern list * term =
@@ -135,6 +137,7 @@ and typeannotation_substitution (s: substitution) (ty: typeannotation) : typeann
   match ty with
     | NoAnnotation -> NoAnnotation
     | Annotation te -> Annotation (term_substitution s te)
+    | TypedAnnotation te -> TypedAnnotation (term_substitution s te)
     | Typed te -> Typed (term_substitution s te)
 
 and destructor_substitution (s: substitution) (des: pattern list * term) : pattern list * term =