diff options
| -rw-r--r-- | kernel/closure.ml | 1 | ||||
| -rw-r--r-- | kernel/closure.mli | 10 | ||||
| -rw-r--r-- | kernel/esubst.ml | 19 | ||||
| -rw-r--r-- | kernel/reduction.ml | 253 | ||||
| -rw-r--r-- | kernel/reduction.mli | 19 | ||||
| -rw-r--r-- | lib/profile.ml | 6 | ||||
| -rw-r--r-- | parsing/g_minicoq.ml4 | 90 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 5 | ||||
| -rw-r--r-- | toplevel/fhimsg.ml | 4 | ||||
| -rw-r--r-- | toplevel/minicoq.ml | 39 |
10 files changed, 228 insertions, 218 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index 541cd7d59..e1469ba48 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -958,6 +958,7 @@ let rec strip_applstack k acc m = let fhnf info v = strip_applstack 0 [] (kh info v []) + let fhnf_apply info k head appl = let stk = zshift k appl in strip_applstack 0 [] (kh info head stk) diff --git a/kernel/closure.mli b/kernel/closure.mli index ef01b73bb..b8d40152a 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -106,7 +106,15 @@ val create: [append_stack] one array at a time but popped with [decomp_stack] one by one *) -type 'a stack +type 'a stack_member = + | Zapp of 'a array * int + | Zcase of case_info * 'a * 'a array + | Zfix of 'a * 'a stack + | Zshift of int + | Zupdate of 'a + +and 'a stack = 'a stack_member list + val empty_stack : 'a stack val append_stack : 'a array -> 'a stack -> 'a stack diff --git a/kernel/esubst.ml b/kernel/esubst.ml index 7d24804cc..46be7a747 100644 --- a/kernel/esubst.ml +++ b/kernel/esubst.ml @@ -22,18 +22,19 @@ type lift = (* i.e under n binders *) (* compose a relocation of magnitude n *) -let rec el_shft n = function - | ELSHFT(el,k) -> el_shft (k+n) el - | el -> if n = 0 then el else ELSHFT(el,n) - +let rec el_shft_rec n = function + | ELSHFT(el,k) -> el_shft_rec (k+n) el + | el -> ELSHFT(el,n) +let el_shft n el = if n = 0 then el else el_shft_rec n el (* cross n binders *) -let rec el_liftn n = function - | ELID -> ELID - | ELLFT(k,el) -> el_liftn (n+k) el - | el -> if n=0 then el else ELLFT(n, el) +let rec el_liftn_rec n = function + | ELID -> ELID + | ELLFT(k,el) -> el_liftn_rec (n+k) el + | el -> ELLFT(n, el) +let el_liftn n el = if n = 0 then el else el_liftn_rec n el -let el_lift el = el_liftn 1 el +let el_lift el = el_liftn_rec 1 el (* relocation of de Bruijn n in an explicit lift *) let rec reloc_rel n = function diff --git a/kernel/reduction.ml b/kernel/reduction.ml index a92fe89ee..5eb519962 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -647,16 +647,13 @@ let whd_betadeltaiota_nolet env sigma x = (********************************************************************) (* Conversion *) (********************************************************************) +(* +let fkey = Profile.declare_profile "fhnf";; +let fhnf info v = Profile.profile2 fkey fhnf info v;; -type conv_pb = - | CONV - | CONV_LEQ - -let pb_is_equal pb = pb = CONV - -let pb_equal = function - | CONV_LEQ -> CONV - | CONV -> CONV +let fakey = Profile.declare_profile "fhnf_apply";; +let fhnf_apply info k h a = Profile.profile4 fakey fhnf_apply info k h a;; +*) type 'a conversion_function = env -> 'a evar_map -> constr -> constr -> constraints @@ -667,52 +664,44 @@ type conversion_test = constraints -> constraints exception NotConvertible -let convert_of_bool b c = - if b then c else raise NotConvertible - -let bool_and_convert b f c = - if b then f c else raise NotConvertible - -let convert_and f1 f2 c = f2 (f1 c) - -let convert_or f1 f2 c = - try f1 c with NotConvertible -> f2 c +(* Convertibility of sorts *) -let convert_forall2 f v1 v2 c = - if Array.length v1 = Array.length v2 - then array_fold_left2 (fun c x y -> f x y c) c v1 v2 - else raise NotConvertible +type conv_pb = + | CONV + | CUMUL -let convert_stacks f v1 v2 c = - convert_forall2 f (array_of_stack v1) (array_of_stack v2) c +let pb_is_equal pb = pb = CONV -(* Convertibility of sorts *) +let pb_equal = function + | CUMUL -> CONV + | CONV -> CONV -let sort_cmp pb s0 s1 = +let sort_cmp pb s0 s1 cuniv = match (s0,s1) with - | (Prop c1, Prop c2) -> convert_of_bool (c1 = c2) - | (Prop c1, Type u) -> convert_of_bool (not (pb_is_equal pb)) + | (Prop c1, Prop c2) -> if c1 = c2 then cuniv else raise NotConvertible + | (Prop c1, Type u) -> + (match pb with + CUMUL -> cuniv + | _ -> raise NotConvertible) | (Type u1, Type u2) -> (match pb with - | CONV -> enforce_eq u1 u2 - | CONV_LEQ -> enforce_geq u2 u1) - | (_, _) -> fun _ -> raise NotConvertible + | CONV -> enforce_eq u1 u2 cuniv + | CUMUL -> enforce_geq u2 u1 cuniv) + | (_, _) -> raise NotConvertible let base_sort_cmp pb s0 s1 = match (s0,s1) with | (Prop c1, Prop c2) -> c1 = c2 - | (Prop c1, Type u) -> not (pb_is_equal pb) + | (Prop c1, Type u) -> pb = CUMUL | (Type u1, Type u2) -> true | (_, _) -> false (* Conversion between [lft1]term1 and [lft2]term2 *) - -let rec ccnv cv_pb infos lft1 lft2 term1 term2 = - eqappr cv_pb infos (lft1, fhnf infos term1) (lft2, fhnf infos term2) +let rec ccnv cv_pb infos lft1 lft2 term1 term2 cuniv = + eqappr cv_pb infos (lft1, fhnf infos term1) (lft2, fhnf infos term2) cuniv (* Conversion between [lft1]([^n1]hd1 v1) and [lft2]([^n2]hd2 v2) *) - -and eqappr cv_pb infos appr1 appr2 = +and eqappr cv_pb infos appr1 appr2 cuniv = let (lft1,(n1,hd1,v1)) = appr1 and (lft2,(n2,hd2,v2)) = appr2 in let el1 = el_shft n1 lft1 @@ -722,114 +711,143 @@ and eqappr cv_pb infos appr1 appr2 = | (FAtom a1, FAtom a2) -> (match kind_of_term a1, kind_of_term a2 with | (IsSort s1, IsSort s2) -> - bool_and_convert - (stack_args_size v1 = 0 && stack_args_size v2 = 0) - (sort_cmp cv_pb s1 s2) + if stack_args_size v1 = 0 && stack_args_size v2 = 0 + then sort_cmp cv_pb s1 s2 cuniv + else raise NotConvertible | (IsMeta n, IsMeta m) -> - bool_and_convert (n=m) - (convert_stacks (ccnv (pb_equal cv_pb) infos lft1 lft2) - v1 v2) - | _ -> fun _ -> raise NotConvertible) + if n=m + then convert_stacks infos lft1 lft2 v1 v2 cuniv + else raise NotConvertible + | _ -> raise NotConvertible) (* 2 index known to be bound to no constant *) | (FRel n, FRel m) -> - bool_and_convert - (reloc_rel n el1 = reloc_rel m el2) - (convert_stacks (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2) + if reloc_rel n el1 = reloc_rel m el2 + then convert_stacks infos lft1 lft2 v1 v2 cuniv + else raise NotConvertible (* 2 constants, 2 existentials or 2 local defined vars or 2 defined rels *) | (FFlex fl1, FFlex fl2) -> - convert_or - (* try first intensional equality *) - (bool_and_convert (fl1 = fl2) - (convert_stacks (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)) + (try (* try first intensional equality *) + if fl1 = fl2 + then + convert_stacks infos lft1 lft2 v1 v2 cuniv + else raise NotConvertible + with NotConvertible -> (* else expand the second occurrence (arbitrary heuristic) *) - (fun u -> - match unfold_reference infos fl2 with - | Some def2 -> - eqappr cv_pb infos appr1 (lft2, fhnf_apply infos n2 def2 v2) u - | None -> (match unfold_reference infos fl1 with - | Some def1 -> eqappr cv_pb infos - (lft1, fhnf_apply infos n1 def1 v1) appr2 u - | None -> raise NotConvertible)) + match unfold_reference infos fl2 with + | Some def2 -> + eqappr cv_pb infos appr1 + (lft2, fhnf_apply infos n2 def2 v2) cuniv + | None -> + (match unfold_reference infos fl1 with + | Some def1 -> + eqappr cv_pb infos + (lft1, fhnf_apply infos n1 def1 v1) appr2 cuniv + | None -> raise NotConvertible)) (* only one constant, existential, defined var or defined rel *) | (FFlex fl1, _) -> (match unfold_reference infos fl1 with | Some def1 -> - eqappr cv_pb infos (lft1, fhnf_apply infos n1 def1 v1) appr2 - | None -> fun _ -> raise NotConvertible) + eqappr cv_pb infos (lft1, fhnf_apply infos n1 def1 v1) + appr2 cuniv + | None -> raise NotConvertible) | (_, FFlex fl2) -> (match unfold_reference infos fl2 with | Some def2 -> - eqappr cv_pb infos appr1 (lft2, fhnf_apply infos n2 def2 v2) - | None -> fun _ -> raise NotConvertible) + eqappr cv_pb infos appr1 + (lft2, fhnf_apply infos n2 def2 v2) + cuniv + | None -> raise NotConvertible) (* other constructors *) | (FLambda (_,c1,c2,_,_), FLambda (_,c'1,c'2,_,_)) -> - bool_and_convert - (stack_args_size v1 = 0 && stack_args_size v2 = 0) - (convert_and - (ccnv (pb_equal cv_pb) infos el1 el2 c1 c'1) - (ccnv (pb_equal cv_pb) infos (el_lift el1) (el_lift el2) c2 c'2)) + if stack_args_size v1 = 0 && stack_args_size v2 = 0 + then + let u1 = ccnv CONV infos el1 el2 c1 c'1 cuniv in + ccnv CONV infos + (el_lift el1) (el_lift el2) c2 c'2 u1 + else raise NotConvertible - | (FLetIn _, _) | (_, FLetIn _) -> anomaly "Normally removed by fhnf" + | (FLetIn _, _) | (_, FLetIn _) -> + anomaly "LetIn normally removed by fhnf" | (FProd (_,c1,c2,_,_), FProd (_,c'1,c'2,_,_)) -> - bool_and_convert - (stack_args_size v1 = 0 && stack_args_size v2 = 0) - (convert_and - (ccnv (pb_equal cv_pb) infos el1 el2 c1 c'1) (* Luo's system *) - (ccnv cv_pb infos (el_lift el1) (el_lift el2) c2 c'2)) + if stack_args_size v1 = 0 && stack_args_size v2 = 0 + then (* Luo's system *) + let u1 = ccnv CONV infos el1 el2 c1 c'1 cuniv in + ccnv cv_pb infos (el_lift el1) (el_lift el2) c2 c'2 u1 + else raise NotConvertible (* Inductive types: MutInd MutConstruct MutCase Fix Cofix *) (* Les annotations du MutCase ne servent qu'à l'affichage *) | (FCases (_,p1,c1,cl1), FCases (_,p2,c2,cl2)) -> - convert_and - (ccnv (pb_equal cv_pb) infos el1 el2 p1 p2) - (convert_and - (ccnv (pb_equal cv_pb) infos el1 el2 c1 c2) - (convert_and - (convert_forall2 (ccnv (pb_equal cv_pb) infos el1 el2) cl1 cl2) - (convert_stacks (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2) - )) + let u1 = ccnv CONV infos el1 el2 p1 p2 cuniv in + let u2 = ccnv CONV infos el1 el2 c1 c2 u1 in + let u3 = convert_vect infos el1 el2 cl1 cl2 u2 in + convert_stacks infos lft1 lft2 v1 v2 u3 | (FInd (op1,cl1), FInd(op2,cl2)) -> - bool_and_convert (op1 = op2) - (convert_and - (convert_forall2 (ccnv (pb_equal cv_pb) infos el1 el2) cl1 cl2) - (convert_stacks (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)) + if op1 = op2 then + let u1 = convert_vect infos el1 el2 cl1 cl2 cuniv in + convert_stacks infos lft1 lft2 v1 v2 u1 + else raise NotConvertible + | (FConstruct (op1,cl1), FConstruct(op2,cl2)) -> - bool_and_convert (op1 = op2) - (convert_and - (convert_forall2 (ccnv (pb_equal cv_pb) infos el1 el2) cl1 cl2) - (convert_stacks (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)) + if op1 = op2 + then + let u1 = convert_vect infos el1 el2 cl1 cl2 cuniv in + convert_stacks infos lft1 lft2 v1 v2 u1 + else raise NotConvertible + | (FFix (op1,(tys1,_,cl1),_,_), FFix(op2,(tys2,_,cl2),_,_)) -> - let n = Array.length cl1 in - bool_and_convert (op1 = op2) - (convert_and - (convert_forall2 (ccnv (pb_equal cv_pb) infos el1 el2) tys1 tys2) - (convert_and - (convert_forall2 (ccnv (pb_equal cv_pb) infos - (el_liftn n el1) (el_liftn n el2)) - cl1 cl2) - (convert_stacks (ccnv (pb_equal cv_pb) infos lft1 lft2) - v1 v2))) + if op1 = op2 + then + let u1 = convert_vect infos el1 el2 tys1 tys2 cuniv in + let n = Array.length cl1 in + let u2 = + convert_vect infos + (el_liftn n el1) (el_liftn n el2) cl1 cl2 u1 in + convert_stacks infos lft1 lft2 v1 v2 u2 + else raise NotConvertible + | (FCoFix (op1,(tys1,_,cl1),_,_), FCoFix(op2,(tys2,_,cl2),_,_)) -> - let n = Array.length cl1 in - bool_and_convert (op1 = op2) - (convert_and - (convert_forall2 (ccnv (pb_equal cv_pb) infos el1 el2) tys1 tys2) - (convert_and - (convert_forall2 (ccnv (pb_equal cv_pb) infos - (el_liftn n el1) (el_liftn n el2)) - cl1 cl2) - (convert_stacks (ccnv (pb_equal cv_pb) infos lft1 lft2) - v1 v2))) + if op1 = op2 + then + let u1 = convert_vect infos el1 el2 tys1 tys2 cuniv in + let n = Array.length cl1 in + let u2 = + convert_vect infos + (el_liftn n el1) (el_liftn n el2) cl1 cl2 u1 in + convert_stacks infos lft1 lft2 v1 v2 u2 + else raise NotConvertible + + | _ -> raise NotConvertible + +and convert_stacks infos lft1 lft2 stk1 stk2 cuniv = + match (decomp_stack stk1, decomp_stack stk2) with + (Some(a1,s1), Some(a2,s2)) -> + let u1 = ccnv CONV infos lft1 lft2 a1 a2 cuniv in + convert_stacks infos lft1 lft2 s1 s2 u1 + | (None, None) -> cuniv + | _ -> raise NotConvertible + +and convert_vect infos lft1 lft2 v1 v2 cuniv = + let lv1 = Array.length v1 in + let lv2 = Array.length v2 in + if lv1 = lv2 + then + let rec fold n univ = + if n >= lv1 then univ + else + let u1 = ccnv CONV infos lft1 lft2 v1.(n) v2.(n) univ in + fold (n+1) u1 in + fold 0 cuniv + else raise NotConvertible - | _ -> (fun _ -> raise NotConvertible) let fconv cv_pb env sigma t1 t2 = @@ -841,15 +859,12 @@ let fconv cv_pb env sigma t1 t2 = Constraint.empty let conv env = fconv CONV env -let conv_leq env = fconv CONV_LEQ env +let conv_leq env = fconv CUMUL env (* let convleqkey = Profile.declare_profile "conv_leq";; -let conv_leq env sigma t1 t2 = Profile.profile4 convleqkey conv_leq env sigma t1 t2;; - - -let convkey = Profile.declare_profile "conv";; -let conv env sigma t1 t2 = Profile.profile4 convleqkey conv env sigma t1 t2;; +let conv_leq env sigma t1 t2 = + Profile.profile4 convleqkey conv_leq env sigma t1 t2;; *) let conv_forall2 f env sigma v1 v2 = @@ -869,7 +884,7 @@ let test_conversion f env sigma x y = let is_conv env sigma = test_conversion conv env sigma let is_conv_leq env sigma = test_conversion conv_leq env sigma -let is_fconv = function | CONV -> is_conv | CONV_LEQ -> is_conv_leq +let is_fconv = function | CONV -> is_conv | CUMUL -> is_conv_leq (********************************************************************) (* Special-Purpose Reduction *) diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 20435a1fc..a47b19242 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -151,31 +151,23 @@ val reduce_fix : local_state_reduction_function -> fixpoint (*s Conversion Functions (uses closures, lazy strategy) *) +type conversion_test = constraints -> constraints + +exception NotConvertible + type conv_pb = | CONV - | CONV_LEQ + | CUMUL val pb_is_equal : conv_pb -> bool val pb_equal : conv_pb -> conv_pb -type conversion_test = constraints -> constraints - -exception NotConvertible - val sort_cmp : conv_pb -> sorts -> sorts -> conversion_test val base_sort_cmp : conv_pb -> sorts -> sorts -> bool -val bool_and_convert : bool -> conversion_test -> conversion_test -val convert_and : conversion_test -> conversion_test -> conversion_test -val convert_or : conversion_test -> conversion_test -> conversion_test -val convert_forall2 : - ('a -> 'b -> conversion_test) -> 'a array -> 'b array -> conversion_test - type 'a conversion_function = env -> 'a evar_map -> constr -> constr -> constraints -val fconv : conv_pb -> 'a conversion_function - (* [fconv] has 2 instances: [conv = fconv CONV] i.e. conversion test, and [conv_leq = fconv CONV_LEQ] i.e. cumulativity test. *) @@ -194,7 +186,6 @@ val is_conv : env -> 'a evar_map -> constr -> constr -> bool val is_conv_leq : env -> 'a evar_map -> constr -> constr -> bool val is_fconv : conv_pb -> env -> 'a evar_map -> constr -> constr -> bool - (*s Special-Purpose Reduction Functions *) val whd_meta : (int * constr) list -> constr -> constr diff --git a/lib/profile.ml b/lib/profile.ml index 825b792d7..f02e6fa5a 100644 --- a/lib/profile.ml +++ b/lib/profile.ml @@ -26,9 +26,9 @@ let get_alloc () = Gc.allocated_bytes () let get_alloc_overhead = let now = get_alloc () in let after = get_alloc () in - after -. now (* Rem: overhead is 16 bytes in ocaml 3.00 *) + after -. now (* Rem: overhead is 16 bytes in ocaml 3.00 *) -let last_alloc = ref 0.0 +let last_alloc = ref (get_alloc()) (* spent_alloc returns a integer in Z/31Z (or Z/63Z) *) (* remark: it cannot detect allocations steps more than 2^31 (or 2^63) *) @@ -122,7 +122,7 @@ let ajoute_to_list ((name,n) as e) l = with Not_found -> e::l let magic = 1249 - + let merge_profile filename (curr_table, curr_outside, curr_total as new_data) = let (old_table, old_outside, old_total) = try diff --git a/parsing/g_minicoq.ml4 b/parsing/g_minicoq.ml4 index 4eec7bb5f..6611eba55 100644 --- a/parsing/g_minicoq.ml4 +++ b/parsing/g_minicoq.ml4 @@ -42,11 +42,6 @@ let inductive = Grammar.Entry.create gram "inductive" let constructor = Grammar.Entry.create gram "constructor" let command = Grammar.Entry.create gram "command" -let new_univ = - let uc = ref 0 in - let univ = id_of_string "univ" in - fun () -> incr uc; { u_sp = make_path [] univ CCI; u_num = !uc } - let path_of_string s = make_path [] (id_of_string s) CCI EXTEND @@ -59,39 +54,39 @@ EXTEND ] ]; term: [ [ id = IDENT -> - VAR (id_of_string id) + mkVar (id_of_string id) | IDENT "Rel"; n = INT -> - Rel (int_of_string n) + mkRel (int_of_string n) | "Set" -> - DOP0 (Sort (Prop Pos)) + mkSet | "Prop" -> - DOP0 (Sort (Prop Null)) + mkProp | "Type" -> - DOP0 (Sort (Type (new_univ()))) + mkType (new_univ()) | "Const"; id = IDENT -> - DOPN (Const (path_of_string id), [||]) + mkConst (path_of_string id, [||]) | "Ind"; id = IDENT; n = INT -> let n = int_of_string n in - DOPN (MutInd (path_of_string id, n), [||]) + mkMutInd ((path_of_string id, n), [||]) | "Construct"; id = IDENT; n = INT; i = INT -> let n = int_of_string n and i = int_of_string i in - DOPN (MutConstruct ((path_of_string id, n), i), [||]) + mkMutConstruct (((path_of_string id, n), i), [||]) | "["; na = name; ":"; t = term; "]"; c = term -> - DOP2 (Lambda, t, DLAM (na, c)) + mkLambda (na,t,c) | "("; na = name; ":"; t = term; ")"; c = term -> - DOP2 (Prod, t, DLAM (na, c)) + mkProd (na,t,c) | c1 = term; "->"; c2 = term -> - DOP2 (Prod, c1, DLAM (Anonymous, c2)) + mkArrow c1 c2 | "("; id = IDENT; cl = LIST1 term; ")" -> - let c = VAR (id_of_string id) in - DOPN (AppL, Array.of_list (c::cl)) + let c = mkVar (id_of_string id) in + mkApp (c, Array.of_list cl) | "("; cl = LIST1 term; ")" -> begin match cl with | [c] -> c - | _ -> DOPN (AppL, Array.of_list cl) + | c::cl -> mkApp (c, Array.of_list cl) end | "("; c = term; "::"; t = term; ")" -> - DOP2 (Cast, c, t) + mkCast (c, t) | "<"; p = term; ">"; IDENT "Case"; c = term; ":"; "Ind"; id = IDENT; i = INT; "of"; bl = LIST0 term; "end" -> @@ -99,7 +94,7 @@ EXTEND let nc = List.length bl in let dummy_pats = Array.create nc RegularPat in let dummy_ci = [||],(ind,[||],nc,None,dummy_pats) in - DOPN (MutCase dummy_ci, Array.of_list (p :: c :: bl)) + mkMutCase (dummy_ci, p, c, Array.of_list bl) ] ]; command: [ [ "Definition"; id = IDENT; ":="; c = term; "." -> @@ -131,17 +126,12 @@ let print_univers = ref false let print_casts = ref false let print_type u = - let sp = u.u_sp and num = u.u_num in - [< 'sTR "Type"; - if !print_univers then - [< 'sTR "("; print_id (basename sp); 'sPC; 'iNT num >] - else - [< >] - >] - + if !print_univers then [< 'sTR "Type"; pr_uni u >] + else [< 'sTR "Type" >] + let print_name = function | Anonymous -> [< 'sTR "_" >] - | Name id -> print_id id + | Name id -> pr_id id let print_rel bv n = print_name (List.nth bv (pred n)) @@ -154,34 +144,34 @@ let rename bv = function in if List.mem na bv then Name (next_ident_away id idl) else na -let rec pp bv = function - | DOP0 (Sort (Prop Pos)) -> [< 'sTR "Set" >] - | DOP0 (Sort (Prop Null)) -> [< 'sTR "Prop" >] - | DOP0 (Sort (Type u)) -> print_type u - | DOP2 (Lambda, t, DLAM(na, c)) -> +let rec pp bv t = + match kind_of_term t with + | IsSort (Prop Pos) -> [< 'sTR "Set" >] + | IsSort (Prop Null) -> [< 'sTR "Prop" >] + | IsSort (Type u) -> print_type u + | IsLambda (na, t, c) -> [< 'sTR"["; print_name na; 'sTR":"; pp bv t; 'sTR"]"; pp (na::bv) c >] - | DOP2 (Prod, t, DLAM(Anonymous, c)) -> + | IsProd (Anonymous, t, c) -> [< pp bv t; 'sTR"->"; pp (Anonymous::bv) c >] - | DOP2 (Prod, t, DLAM(na, c)) -> + | IsProd (na, t, c) -> [< 'sTR"("; print_name na; 'sTR":"; pp bv t; 'sTR")"; pp (na::bv) c >] - | DOP2 (Cast, c, t) -> + | IsCast (c, t) -> if !print_casts then [< 'sTR"("; pp bv c; 'sTR"::"; pp bv t; 'sTR")" >] else pp bv c - | DOPN (AppL, [|c|]) -> - pp bv c - | DOPN (AppL, v) -> - [< 'sTR"("; prvect_with_sep (fun () -> [< 'sPC >]) (pp bv) v; 'sTR")" >] - | DOPN (Const sp, _) -> - [< 'sTR"Const "; print_id (basename sp) >] - | DOPN (MutInd (sp,i), _) -> - [< 'sTR"Ind "; print_id (basename sp); 'sTR" "; 'iNT i >] - | DOPN (MutConstruct ((sp,i),j), _) -> - [< 'sTR"Construct "; print_id (basename sp); 'sTR" "; 'iNT i; + | IsApp(h, v) -> + [< 'sTR"("; pp bv h; 'sPC; + prvect_with_sep (fun () -> [< 'sPC >]) (pp bv) v; 'sTR")" >] + | IsConst (sp, _) -> + [< 'sTR"Const "; pr_id (basename sp) >] + | IsMutInd ((sp,i), _) -> + [< 'sTR"Ind "; pr_id (basename sp); 'sTR" "; 'iNT i >] + | IsMutConstruct (((sp,i),j), _) -> + [< 'sTR"Construct "; pr_id (basename sp); 'sTR" "; 'iNT i; 'sTR" "; 'iNT j >] - | VAR id -> print_id id - | Rel n -> print_rel bv n + | IsVar id -> pr_id id + | IsRel n -> print_rel bv n | _ -> [< 'sTR"<???>" >] let pr_term _ ctx = pp (fold_rel_context (fun _ (n,_,_) l -> n::l) ctx []) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 7a1423c3c..a891cdd03 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -20,7 +20,6 @@ open Classops open Recordops open Evarutil - type flexible_term = FConst of constant | FRel of int | FVar of identifier type flex_kind_of_term = | Rigid of constr @@ -314,6 +313,6 @@ and check_conv_record (t1,l1) (t2,l2) = with _ -> raise Not_found -let the_conv_x env isevars t1 t2 = evar_conv_x env isevars CONV t1 t2 -let the_conv_x_leq env isevars t1 t2 = evar_conv_x env isevars CONV_LEQ t1 t2 +let the_conv_x env isevars t1 t2 = evar_conv_x env isevars CONV t1 t2 +let the_conv_x_leq env isevars t1 t2 = evar_conv_x env isevars CUMUL t1 t2 diff --git a/toplevel/fhimsg.ml b/toplevel/fhimsg.ml index d76fba078..70d830ef5 100644 --- a/toplevel/fhimsg.ml +++ b/toplevel/fhimsg.ml @@ -314,10 +314,12 @@ let explain_type_error k ctx = function explain_ill_formed_rec_body k ctx i lna vdefj vargs | IllTypedRecBody (i, lna, vdefj, vargs) -> explain_ill_typed_rec_body k ctx i lna vdefj vargs +(* | NotInductive c -> explain_not_inductive k ctx c | MLCase (mes,c,ct,br,brt) -> explain_ml_case k ctx mes c ct br brt +*) | _ -> [< 'sTR "Unknown type error (TODO)" >] @@ -348,7 +350,7 @@ let explain_occur_check k ctx ev rhs = 'sTR" with term"; 'bRK(1,1); pt >] let explain_not_clean k ctx sp t = - let c = Rel (Intset.choose (free_rels t)) in + let c = mkRel (Intset.choose (free_rels t)) in let id = string_of_id (Names.basename sp) in let var = P.pr_term k ctx c in errorlabstrm "Trad.not_clean" diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml index 148033c7f..b4affe6c1 100644 --- a/toplevel/minicoq.ml +++ b/toplevel/minicoq.ml @@ -21,15 +21,19 @@ open G_minicoq let (env : safe_environment ref) = ref empty_environment +let locals () = + List.map (fun (id,b,t) -> (id, make_path [] id CCI)) + (named_context !env) + let lookup_named id = let rec look n = function | [] -> mkVar id - | (Name id')::_ when id = id' -> Rel n + | (Name id')::_ when id = id' -> mkRel n | _::r -> look (succ n) r in look 1 -let args sign = Array.of_list (List.map mkVar (ids_of_named_context sign)) +let args sign = Array.of_list (instance_from_section_context sign) let rec globalize bv c = match kind_of_term c with | IsVar id -> lookup_named id bv @@ -51,15 +55,15 @@ let check c = let definition id ty c = let c = globalize [] c in let ty = option_app (globalize []) ty in - let ce = { const_entry_body = Cooked c; const_entry_type = ty } in + let ce = { const_entry_body = c; const_entry_type = ty } in let sp = make_path [] id CCI in - env := add_constant sp ce !env; + env := add_constant sp ce (locals()) !env; mSGNL (hOV 0 [< pr_id id; 'sPC; 'sTR"is defined"; 'fNL >]) let parameter id t = let t = globalize [] t in let sp = make_path [] id CCI in - env := add_parameter sp t !env; + env := add_parameter sp t (locals()) !env; mSGNL (hOV 0 [< 'sTR"parameter"; 'sPC; pr_id id; 'sPC; 'sTR"is declared"; 'fNL >]) @@ -69,31 +73,30 @@ let variable id t = mSGNL (hOV 0 [< 'sTR"variable"; 'sPC; pr_id id; 'sPC; 'sTR"is declared"; 'fNL >]) -let put_DLAMSV lna lc = - match lna with - | [] -> anomaly "put_DLAM" - | na::lrest -> List.fold_left (fun c na -> DLAM(na,c)) (DLAMV(na,lc)) lrest - let inductive par inds = let nparams = List.length par in let bvpar = List.rev (List.map (fun (id,_) -> Name id) par) in let name_inds = List.map (fun (id,_,_) -> Name id) inds in let bv = bvpar @ List.rev name_inds in - let par = List.map (fun (id,c) -> (Name id, globalize [] c)) par in + let npar = List.map (fun (id,c) -> (Name id, globalize [] c)) par in let one_inductive (id,ar,cl) = - let cv = Array.of_list (List.map snd cl) in - let cv = Array.map (fun c -> prod_it (globalize bv c) par) cv in - let c = put_DLAMSV name_inds cv in - (id, prod_it (globalize bvpar ar) par, List.map fst cl, [c]) + let cv = List.map (fun (_,c) -> prod_it (globalize bv c) npar) cl in + { mind_entry_nparams = nparams; + mind_entry_params = List.map (fun (id,c) -> (id, LocalAssum c)) par; + mind_entry_typename = id; + mind_entry_arity = prod_it (globalize bvpar ar) npar; + mind_entry_consnames = List.map fst cl; + mind_entry_lc = cv } in let inds = List.map one_inductive inds in let mie = { - mind_entry_nparams = nparams; mind_entry_finite = true; mind_entry_inds = inds } in - let sp = let (id,_,_,_) = List.hd inds in make_path [] id CCI in - env := add_mind sp mie !env; + let sp = + let mi1 = List.hd inds in + make_path [] mi1.mind_entry_typename CCI in + env := add_mind sp mie (locals()) !env; mSGNL (hOV 0 [< 'sTR"inductive type(s) are declared"; 'fNL >]) |