diff --git a/src/API.ml b/src/API.ml index 1004ec0ee..f72e1dda1 100644 --- a/src/API.ml +++ b/src/API.ml @@ -208,7 +208,7 @@ module RawOpaqueData = struct = let ty = Conversion.TyName name in let embed ~depth:_ _ _ state x = - state, ED.Term.CData (cin x), [] in + state, ED.Term.Pure.mkCData (cin x), [] in let readback ~depth _ _ state t = let module R = (val !r) in let open R in match R.deref_head ~depth t with @@ -292,21 +292,21 @@ module BuiltInData = struct let open ED in let rec aux d t = match deref_head ~depth:(depth + d) t with - | Lam t -> mkLam (aux (d+1) t) + | Lam t -> Heap.mkLam (aux (d+1) t) | Const c as x -> if c < 0 || c >= depth then x else raise Conversion.(TypeErr(TyName"closed term",depth+d,x)) | App (c,x,xs) -> - if c < 0 || c >= depth then mkApp c (aux d x) (List.map (aux d) xs) + if c < 0 || c >= depth then Heap.mkApp c (aux d x) (List.map (aux d) xs) else raise Conversion.(TypeErr(TyName"closed term",depth+d,x)) | (UVar _ | AppUVar _) as x -> raise Conversion.(TypeErr(TyName"closed term",depth+d,x)) - | Arg _ | AppArg _ -> assert false - | Builtin (c,xs) -> mkBuiltin c (List.map (aux d) xs) + | Builtin (c,xs) -> Heap.mkBuiltin c (List.map (aux d) xs) | CData _ as x -> x - | Cons (hd,tl) -> mkCons (aux d hd) (aux d tl) + | Cons (hd,tl) -> Heap.mkCons (aux d hd) (aux d tl) | Nil as x -> x - | Discard as x -> x + | XArg _ | XAppArg _ -> assert false + | (XDiscard _ | XApp _ | XCons _ | XBuiltin _ | XLam _) -> assert false in (aux 0 t, depth) @@ -366,7 +366,7 @@ module Elpi = struct | Arg str -> Format.fprintf fmt "%s" str | Ref ub -> - Pp.term fmt (ED.mkUVar ub lvl 0) + Pp.term fmt (ED.Heap.mkUVar ub lvl 0) let show m = Format.asprintf "%a" pp m @@ -427,22 +427,23 @@ module RawData = struct type view = (* Pure subterms *) | Const of constant (* global constant or a bound var *) + | CData of RawOpaqueData.t (* external data *) + | Nil (* [] *) + | Lam of term (* lambda abstraction, i.e. x\ *) | App of constant * term * term list (* application (at least 1 arg) *) - (* Optimizations *) - | Cons of term * term (* :: *) - | Nil (* [] *) - | Discard (* _ *) (* FFI *) | Builtin of builtin * term list (* call to a built-in predicate *) - | CData of RawOpaqueData.t (* external data *) + (* Optimizations *) + | Cons of term * term (* :: *) (* Unassigned unification variables *) | UnifVar of Elpi.t * term list let look ~depth t = let module R = (val !r) in let open R in match R.deref_head ~depth t with - | ED.Term.Arg _ | ED.Term.AppArg _ -> assert false + | ED.Term.XArg _ | ED.Term.XAppArg _ -> assert false + | ED.Term.XLam _ | ED.Term.XApp _ | ED.Term.XCons _ | ED.Term.XBuiltin _ -> assert false | ED.Term.UVar(ub,lvl,nargs) -> let args = ED.Term.Constants.mkinterval 0 nargs 0 in UnifVar ({ lvl; handle = Ref ub},args) @@ -451,19 +452,20 @@ module RawData = struct | x -> Obj.magic x (* HACK: view is a "subtype" of Term.term *) let kool = function - | UnifVar({ lvl; handle = Ref ub},args) -> ED.Term.AppUVar(ub,lvl,args) + | UnifVar({ lvl; handle = Ref ub},args) -> + (* TODO: Use the runtime one *) + ED.Term.Heap.mkAppUVar ub lvl args | UnifVar({ lvl; handle = Arg _},_) -> assert false | x -> Obj.magic x [@@ inline] - let mkConst = ED.Term.mkConst - let mkLam = ED.Term.mkLam - let mkApp = ED.Term.mkApp - let mkCons = ED.Term.mkCons - let mkNil = ED.Term.mkNil - let mkDiscard = ED.Term.mkDiscard - let mkBuiltin = ED.Term.mkBuiltin - let mkCData = ED.Term.mkCData + let mkConst = ED.Term.Constants.mkConst + let mkLam = ED.Term.Heap.mkLam + let mkApp = ED.Term.Heap.mkApp + let mkCons = ED.Term.Heap.mkCons + let mkNil = ED.Term.Pure.mkNil + let mkBuiltin = ED.Term.Heap.mkBuiltin + let mkCData = ED.Term.Pure.mkCData let mkAppL = ED.Term.mkAppL let mkAppS = ED.Term.mkAppS let mkAppSL = ED.Term.mkAppSL @@ -505,7 +507,7 @@ module RawData = struct let mkUnifVar { Elpi.handle; lvl } ~args state = match handle with - | Elpi.Ref ub -> ED.Term.mkAppUVar ub lvl args + | Elpi.Ref ub -> ED.Term.Heap.mkAppUVar ub lvl args | Elpi.Arg name -> Compiler.get_Arg state ~name ~args end @@ -620,9 +622,6 @@ module FlexibleData = struct embed = (fun ~depth _ _ s (k,args) -> s, RawData.mkUnifVar k ~args s, []); readback = (fun ~depth _ _ state t -> match RawData.look ~depth t with - | RawData.Discard -> - let state, k = Elpi.make ~lvl:depth state in - state, (k,[]), [] | RawData.UnifVar(k,args) -> state, (k,args), [] | _ -> raise (Conversion.TypeErr (TyName "uvar",depth,t))); @@ -726,38 +725,34 @@ module Utils = struct let clause_of_term ?name ?graft ~depth loc term = let open EA in - let module Data = ED.Term in - let module R = (val !r) in let open R in let rec aux d ctx t = - match R.deref_head ~depth:d t with - | Data.Const i when i >= 0 && i < depth -> + match RawData.look ~depth:d t with + | RawData.Const i when i >= 0 && i < depth -> error "program_of_term: the term is not closed" - | Data.Const i when i < 0 -> - Term.mkCon (Data.Constants.show i) - | Data.Const i -> Util.IntMap.find i ctx - | Data.Lam t -> + | RawData.Const i when i < 0 -> + Term.mkCon (ED.Constants.show i) + | RawData.Const i -> Util.IntMap.find i ctx + | RawData.Lam t -> let s = "x" ^ string_of_int d in let ctx = Util.IntMap.add d (Term.mkCon s) ctx in Term.mkLam s (aux (d+1) ctx t) - | Data.App(c,x,xs) -> - let c = aux d ctx (Data.Constants.mkConst c) in + | RawData.App(c,x,xs) -> + let c = aux d ctx (ED.Constants.mkConst c) in let x = aux d ctx x in let xs = List.map (aux d ctx) xs in Term.mkApp loc (c :: x :: xs) - | (Data.Arg _ | Data.AppArg _) -> assert false - | Data.Cons(hd,tl) -> + | RawData.Cons(hd,tl) -> let hd = aux d ctx hd in let tl = aux d ctx tl in Term.mkSeq [hd;tl] - | Data.Nil -> Term.mkNil - | Data.Builtin(c,xs) -> - let c = aux d ctx (Data.Constants.mkConst c) in + | RawData.Nil -> Term.mkNil + | RawData.Builtin(c,xs) -> + let c = aux d ctx (ED.Constants.mkConst c) in let xs = List.map (aux d ctx) xs in Term.mkApp loc (c :: xs) - | Data.CData x -> Term.mkC x - | (Data.UVar _ | Data.AppUVar _) -> + | RawData.CData x -> Term.mkC x + | RawData.UnifVar _ -> error "program_of_term: the term contains uvars" - | Data.Discard -> Term.mkCon "_" in let attributes = (match name with Some x -> [Clause.Name x] | None -> []) @ diff --git a/src/API.mli b/src/API.mli index 47216e17c..d715e1ca6 100644 --- a/src/API.mli +++ b/src/API.mli @@ -757,17 +757,15 @@ module RawData : sig type builtin type term = Data.term type view = private - (* Pure subterms *) | Const of constant (* global constant or a bound var *) + | CData of RawOpaqueData.t (* external data *) + | Nil (* [] *) | Lam of term (* lambda abstraction, i.e. x\ *) | App of constant * term * term list (* application (at least 1 arg) *) - (* Optimizations *) - | Cons of term * term (* :: *) - | Nil (* [] *) - | Discard (* _ *) (* FFI *) | Builtin of builtin * term list (* call to a built-in predicate *) - | CData of RawOpaqueData.t (* opaque data *) + (* Optimizations *) + | Cons of term * term (* :: *) (* Unassigned unification variables *) | UnifVar of FlexibleData.Elpi.t * term list @@ -787,7 +785,6 @@ module RawData : sig val mkAppSL : string -> term list -> term val mkCons : term -> term -> term val mkNil : term - val mkDiscard : term val mkBuiltinS : string -> term list -> term val mkCData : RawOpaqueData.t -> term val mkUnifVar : FlexibleData.Elpi.t -> args:term list -> State.t -> term diff --git a/src/builtin.ml b/src/builtin.ml index aefdfb877..b07c00870 100644 --- a/src/builtin.ml +++ b/src/builtin.ml @@ -61,7 +61,6 @@ let rec eval depth t = f [] | (Nil | Cons _ as x) -> type_error ("Lists cannot be evaluated: " ^ RawPp.Debug.show_term (kool x)) - | Discard -> type_error "_ cannot be evaluated" | CData _ as x -> kool x ;; @@ -183,7 +182,6 @@ let occurs x d t = | Builtin (_, vs) -> auxs vs | Cons (v1, v2) -> aux v1 || aux v2 | Nil - | Discard | CData _ -> false and auxs = function | [] -> false @@ -738,7 +736,6 @@ let name_or_constant name condition = (); fun x out ~depth _ _ state -> | NoData -> raise No_clause | Data x -> match look ~depth x with - | Discard -> assert false | Const n when condition n -> if out = [] then !: x +? None else !: x +! [Some x; Some mkNil] @@ -763,8 +760,6 @@ let name_or_constant name condition = (); fun x out ~depth _ _ state -> let rec same_term ~depth t1 t2 = match look ~depth t1, look ~depth t2 with - | Discard, UnifVar _ -> true - | UnifVar _, Discard -> true | UnifVar(b1,xs), UnifVar(b2,ys) -> FlexibleData.Elpi.equal b1 b2 && same_term_list ~depth xs ys | App(c1,x,xs), App(c2,y,ys) -> c1 == c2 && same_term ~depth x y && same_term_list ~depth xs ys | Const c1, Const c2 -> c1 == c2 diff --git a/src/compiler.ml b/src/compiler.ml index 888524257..a5b081c2c 100644 --- a/src/compiler.ml +++ b/src/compiler.ml @@ -460,7 +460,7 @@ let mk_Arg state ~name ~args = with Not_found -> update_argmap state (mk_Arg name) in match args with | [] -> state, t - | x::xs -> state, App(c,x,xs) + | x::xs -> state, Stack.mkApp c x xs let get_Arg state ~name ~args = let { n2t } = get_argmap state in @@ -469,7 +469,7 @@ let get_Arg state ~name ~args = with Not_found -> error "get_Arg" in match args with | [] -> t - | x::xs -> App(c,x,xs) + | x::xs -> Stack.mkApp c x xs let fresh_Arg = let qargno = ref 0 in @@ -504,13 +504,13 @@ let preterm_of_ast loc ~depth:arg_lvl macro state ast = try state, F.Map.find f (get_varmap state) with Not_found -> if is_discard f then - state, Discard + state, Stack.mkDiscard () else if is_uvar_name f then mk_Arg state ~name:(F.show f) ~args:[] else if is_macro_name f then stack_macro_of_ast inner curlvl state f else if BuiltInPredicate.is_declared (fst (C.funct_of_ast f)) then - state, Builtin(fst (C.funct_of_ast f),[]) + state, Stack.mkBuiltin (fst (C.funct_of_ast f)) [] else if CustomFunctorCompilation.is_backtick f then CustomFunctorCompilation.compile_backtick state f else if CustomFunctorCompilation.is_singlequote f then @@ -518,12 +518,12 @@ let preterm_of_ast loc ~depth:arg_lvl macro state ast = else state, snd (C.funct_of_ast f) and aux inner lvl state = function - | Ast.Term.Const f when F.(equal f nilf) -> state, Term.Nil + | Ast.Term.Const f when F.(equal f nilf) -> state, Pure.mkNil | Ast.Term.Const f -> stack_funct_of_ast inner lvl state f | Ast.Term.App(Ast.Term.Const f, [hd;tl]) when F.(equal f consf) -> let state, hd = aux true lvl state hd in let state, tl = aux true lvl state tl in - state, Term.Cons(hd,tl) + state, Stack.mkCons hd tl | Ast.Term.App(Ast.Term.Const f, tl) -> let state, rev_tl = List.fold_left (fun (state, tl) t -> @@ -534,14 +534,14 @@ let preterm_of_ast loc ~depth:arg_lvl macro state ast = let state, c = stack_funct_of_ast inner lvl state f in begin match c with | Const c -> begin match tl with - | hd2::tl -> state, Term.App(c,hd2,tl) + | hd2::tl -> state, Stack.mkApp c hd2 tl | _ -> anomaly "Application node with no arguments" end - | App(c,hd1,tl1) -> (* FG:decurrying: is this the right place for it? *) - state, Term.App(c,hd1,tl1@tl) - | Builtin(c,tl1) -> state, Term.Builtin(c,tl1@tl) - | Lam _ -> (* macro with args *) + | XApp(c,hd1,tl1) -> (* FG:decurrying: is this the right place for it? *) + state, Stack.mkApp c hd1 (tl1@tl) + | XBuiltin(c,tl1) -> state, Stack.mkBuiltin c (tl1@tl) + | XLam _ -> (* macro with args *) state, R.deref_appuv ~from:lvl ~to_:lvl tl c - | Discard -> + | XDiscard () -> error ~loc "Clause shape unsupported: _ cannot be applied" | _ -> error ~loc "Clause shape unsupported" end (* @@ -556,15 +556,15 @@ let preterm_of_ast loc ~depth:arg_lvl macro state ast = *) | Ast.Term.Lam (x,t) when F.(equal x dummyname)-> let state, t' = aux true (lvl+1) state t in - state, Term.Lam t' + state, Stack.mkLam t' | Ast.Term.Lam (x,t) -> let orig_varmap = get_varmap state in - let state = update_varmap state (F.Map.add x (mkConst lvl)) in + let state = update_varmap state (F.Map.add x (Constants.mkConst lvl)) in let state, t' = aux true (lvl+1) state t in - set_varmap state orig_varmap, Term.Lam t' + set_varmap state orig_varmap, Stack.mkLam t' | Ast.Term.App (Ast.Term.App (f,l1),l2) -> aux inner lvl state (Ast.Term.App (f, l1@l2)) - | Ast.Term.CData c -> state, Term.CData (CData.hcons c) + | Ast.Term.CData c -> state, Pure.mkCData (CData.hcons c) | Ast.Term.App (Ast.Term.Lam _,_) -> error ~loc "Beta-redexes not in our language" | Ast.Term.App (Ast.Term.CData _,_) -> type_error ~loc "Applied literal" | Ast.Term.Quoted { Ast.Term.data; kind = None; loc } -> @@ -730,12 +730,12 @@ let query_preterm_of_ast ~depth macros state (loc, t) = let global_hd_symbols_of_clauses cl = List.fold_left (fun s { Ast.Clause.body = { term } } -> match term with - | (Const c | App(c,_,_)) when c != C.rimplc && c < 0 -> + | (Const c | XApp(c,_,_)) when c != C.rimplc && c < 0 -> C.Set.add c s - | App(ri,(Const c | App(c,_,_)), _) when ri == C.rimplc && c < 0 -> + | XApp(ri,(Const c | XApp(c,_,_)), _) when ri == C.rimplc && c < 0 -> C.Set.add c s - | (Const _ | App _) -> s - | Builtin(c,_) -> C.Set.add c s + | (Const _ | XApp _) -> s + | XBuiltin(c,_) -> C.Set.add c s | _ -> assert false) C.Set.empty cl @@ -749,11 +749,7 @@ let query_preterm_of_ast ~depth macros state (loc, t) = (* Printf.eprintf "%s -> %s\n" (C.show c) (C.show c'); *) c' - let prepend p s = - (* XXX OCaml 4.04: C.Set.map (prefix_const [p]) s *) - let res = ref C.Set.empty in - C.Set.iter (fun x -> res := C.Set.add (prefix_const [p] x) !res) s; - !res + let prepend p s = C.Set.map (prefix_const [p]) s let run ~flags:_ state p = @@ -780,7 +776,7 @@ let query_preterm_of_ast ~depth macros state (loc, t) = let orig_varmap = get_varmap state in let lcs, state = List.fold_left (fun (lcs,state) name -> - let rel = mkConst lcs in + let rel = Constants.mkConst lcs in lcs+1, update_varmap state (F.Map.add name rel)) (lcs,state) nlist in let state, lcs, _, @@ -862,76 +858,44 @@ end = struct (* {{{ *) (* Customs are already translated inside terms, * may sill require translation inside type/modes declaration *) - let smart_map_term f t = - let rec aux = function - | Const c as x -> - let c1 = f c in - if c == c1 then x else mkConst c1 - | Lam t as x -> - let t1 = aux t in - if t == t1 then x else Lam t1 - | AppArg(i,ts) as x -> - let ts1 = smart_map aux ts in - if ts == ts1 then x else AppArg(i,ts1) - | AppUVar(r,lvl,ts) as x -> - assert(!!r == C.dummy); - let ts1 = smart_map aux ts in - if ts == ts1 then x else AppUVar(r,lvl,ts1) - | Builtin(c,ts) as x -> - if f c != c then - error ("declaring a clause for builtin: " ^ Constants.show c); - let ts1 = smart_map aux ts in - if ts == ts1 then x else Builtin(c,ts1) - | App(c,t,ts) as x -> - let c1 = f c in - let t1 = aux t in - let ts1 = smart_map aux ts in - if c == c1 && t == t1 && ts == ts1 then x else App(c1,t1,ts1) - | Cons(hd,tl) as x -> - let hd1 = aux hd in - let tl1 = aux tl in - if hd == hd1 && tl == tl1 then x else Cons(hd1,tl1) - | UVar(r,_,_) as x -> - assert(!!r == C.dummy); - x - | (Arg _ | CData _ | Nil | Discard) as x -> x - in - aux t - let smart_map_type f ({ Structured.loc; tindex; decl = { tname; ttype }} as tdecl) = let tname1 = f tname in - let ttype1 = smart_map_term f ttype.term in + (* XX This check has gone! + if f c != c then + error ("declaring a clause for builtin: " ^ Constants.show c); + *) + let ttype1 = Term.smart_map f ttype.term in if tname1 == tname && ttype1 == ttype.term then tdecl else { Structured.loc; tindex; decl = { tname = tname1; ttype = { term = ttype1; amap = ttype.amap; loc = ttype.loc } } } let map_sequent f { peigen; pcontext; pconclusion } = { - peigen = smart_map_term f peigen; - pcontext = smart_map_term f pcontext; - pconclusion =smart_map_term f pconclusion; + peigen = Term.smart_map f peigen; + pcontext = Term.smart_map f pcontext; + pconclusion = Term.smart_map f pconclusion; } let map_chr f { pto_match; pto_remove; pguard; pnew_goal; pamap; pifexpr; pname; pcloc } = { - pto_match = smart_map (map_sequent f) pto_match; - pto_remove = smart_map (map_sequent f) pto_remove; - pguard = option_map (smart_map_term f) pguard; + pto_match = Util.smart_map (map_sequent f) pto_match; + pto_remove = Util.smart_map (map_sequent f) pto_remove; + pguard = option_map (Term.smart_map f) pguard; pnew_goal = option_map (map_sequent f) pnew_goal; pamap; pifexpr; pname; pcloc; } let map_clause f ({ Ast.Clause.body = { term; amap; loc } } as x) = - { x with Ast.Clause.body = { term = smart_map_term f term; amap; loc } } + { x with Ast.Clause.body = { term = Term.smart_map f term; amap; loc } } type subst = (string list * (C.t -> C.t)) let apply_subst (f : (C.t -> C.t) -> 'a -> 'a) (s : subst) : 'a -> 'a = fun x -> f (snd s) x - let apply_subst_list f = apply_subst (fun x -> smart_map (f x)) + let apply_subst_list f = apply_subst (fun x -> Util.smart_map (f x)) let apply_subst_constant = apply_subst (fun f x -> f x) @@ -1021,8 +985,8 @@ module Spill : sig end = struct (* {{{ *) let rec read_ty = function - | App(c,x,[y]) when c == C.variadic -> `Variadic (read_ty x,read_ty y) - | App(c,x,[y]) when c == C.arrowc -> + | XApp(c,x,[y]) when c == C.variadic -> `Variadic (read_ty x,read_ty y) + | XApp(c,x,[y]) when c == C.arrowc -> let ty_x = read_ty x in begin match read_ty y with | `Arrow(tys,ty) -> `Arrow (ty_x :: tys, ty) @@ -1041,12 +1005,12 @@ end = struct (* {{{ *) let missing_args_of loc modes types t = let c, args = let rec aux = function - | App (c,_,[x]) when c == C.implc -> aux x - | App (c,x,xs) when c == C.andc || c == C.andc2 -> + | XApp (c,_,[x]) when c == C.implc -> aux x + | XApp (c,x,xs) when c == C.andc || c == C.andc2 -> aux List.(hd (rev (x :: xs))) - | App (c,x,xs) -> c, x :: xs + | XApp (c,x,xs) -> c, x :: xs | Const c -> c, [] - | Builtin(c,args) -> c, args + | XBuiltin(c,args) -> c, args | _ -> error ~loc "Only applications can be spilled" in aux t in @@ -1083,14 +1047,14 @@ end = struct (* {{{ *) x in let mkAppC c = function - | [] -> mkConst c - | x::xs -> App(c,x,xs) in + | [] -> Constants.mkConst c + | x::xs -> Stack.mkApp c x xs in let mkApp hd args = match hd with - | App(c,x,xs) -> App(c,x,xs @ args) + | XApp(c,x,xs) -> Stack.mkApp c x (xs @ args) | Const c -> mkAppC c args - | Builtin(c,xs) -> Builtin(c,xs @ args) + | XBuiltin(c,xs) -> Stack.mkBuiltin c (xs @ args) | _ -> assert false in let mkSpilled = @@ -1111,9 +1075,9 @@ end = struct (* {{{ *) | x::xs -> x :: on_last f xs in let rec aux = function - | App(c,x,[y]) when c == C.implc -> + | XApp(c,x,[y]) when c == C.implc -> mkAppC c [x;aux y] - | App (c,x,xs) when c == C.andc || c == C.andc2 -> + | XApp (c,x,xs) when c == C.andc || c == C.andc2 -> mkAppC c (on_last aux (x::xs)) | t -> mkApp t args in @@ -1122,48 +1086,49 @@ end = struct (* {{{ *) let rec apply_to names variable = function | Const f as x when List.exists (equal_term x) names -> mkAppC f [variable] - | (Const _ | CData _ | Nil | Discard) as x -> x - | Cons(hd,tl) -> - Cons(apply_to names variable hd,apply_to names variable tl) - | Lam t -> Lam (apply_to names variable t) - | App(f,x,xs) when List.exists (equal_term (Const f)) names -> + | (Const _ | CData _ | Nil | XDiscard _) as x -> x + | XCons(hd,tl) -> + Stack.mkCons (apply_to names variable hd) (apply_to names variable tl) + | XLam t -> Stack.mkLam (apply_to names variable t) + | XApp(f,x,xs) when List.exists (equal_term (Pure.mkConst f)) names -> mkAppC f (List.map (apply_to names variable) (x::xs) @ [variable]) - | App(hd,x,xs) -> mkAppC hd (List.map (apply_to names variable) (x::xs)) - | Builtin(hd,xs) -> Builtin(hd, List.map (apply_to names variable) xs) - | (Arg _ | AppArg _ | UVar _ | AppUVar _) -> assert false in + | XApp(hd,x,xs) -> mkAppC hd (List.map (apply_to names variable) (x::xs)) + | XBuiltin(hd,xs) -> Stack.mkBuiltin hd (List.map (apply_to names variable) xs) + | (XArg _ | XAppArg _ | UVar _ | AppUVar _) -> assert false + | (App _ | Cons _ | Lam _ | Builtin _) -> assert false in let add_spilled sp t = if sp = [] then t else mkAppC C.andc (List.map snd sp @ [t]) in let rec spaux (depth,vars as ctx) = function - | App(c, fcall, rest) when c == C.spillc -> + | XApp(c, fcall, rest) when c == C.spillc -> assert (rest = []); let spills, fcall = spaux1 ctx fcall in let args = mkSpilled (List.rev vars) (missing_args_of loc modes types fcall) in spills @ [args, mkAppSpilled fcall args], args - | App(c, Lam arg, []) when c == C.pic -> - let ctx = depth+1, mkConst depth :: vars in + | XApp(c, XLam arg, []) when c == C.pic -> + let ctx = depth+1, Constants.mkConst depth :: vars in let spills, arg = spaux1 ctx arg in - [], [mkAppC c [Lam (add_spilled spills arg)]] - | App(c, Lam arg, []) when c == C.sigmac -> + [], [mkAppC c [Stack.mkLam (add_spilled spills arg)]] + | XApp(c, XLam arg, []) when c == C.sigmac -> let ctx = depth+1, vars in let spills, arg = spaux1 ctx arg in - [], [mkAppC c [Lam (add_spilled spills arg)]] - | App(c, hyp, [concl]) when c == C.implc -> + [], [mkAppC c [Stack.mkLam (add_spilled spills arg)]] + | XApp(c, hyp, [concl]) when c == C.implc -> let spills_hyp, hyp1 = spaux1 ctx hyp in let t = spaux1_prop ctx concl in if (spills_hyp != []) then error ~loc "Cannot spill in the head of a clause"; [], [mkAppC c (hyp1 :: t)] - | App(c, concl, [hyp]) when c == C.rimplc -> + | XApp(c, concl, [hyp]) when c == C.rimplc -> let t = spaux1_prop ctx hyp in let spills_concl, concl1 = spaux1 ctx concl in if (spills_concl != []) then error ~loc "Cannot spill in the head of a clause"; [], [mkAppC c (concl1 :: t)] - | App(hd,x,xs) -> + | XApp(hd,x,xs) -> let args = x :: xs in let spills, args, is_prop = let (@@@) (s1,a1) (s2,a2,b) = s1 @ s2, a1 @ a2, b in @@ -1181,29 +1146,30 @@ end = struct (* {{{ *) aux (type_of_const types hd) args in if is_prop then [], [add_spilled spills (mkAppC hd args)] else spills, [mkAppC hd args] - | (CData _ | Const _ | Discard | Nil) as x -> [],[x] - | Cons(hd,tl) -> + | (CData _ | Const _ | XDiscard () | Nil) as x -> [],[x] + | XCons(hd,tl) -> let sp1, hd = spaux ctx hd in let sp2, tl = spaux ctx tl in (* FIXME: it could be in prop *) assert(List.length hd = 1 && List.length tl = 1); - sp1 @ sp2, [Cons(List.hd hd, List.hd tl)] - | Builtin(c,args) -> + sp1 @ sp2, [Stack.mkCons (List.hd hd) (List.hd tl)] + | XBuiltin(c,args) -> let spills, args = map_acc (fun sp x -> let sp1, x = spaux ctx x in sp @ sp1, x) [] args in - [], [add_spilled spills (Builtin(c,List.concat args))] - | Lam t -> - let sp, t = spaux1 (depth+1, mkConst depth :: vars) t in + [], [add_spilled spills (Stack.mkBuiltin c (List.concat args))] + | XLam t -> + let sp, t = spaux1 (depth+1, Constants.mkConst depth :: vars) t in let (t,_), sp = map_acc (fun (t,n) (names, call) -> let all_names = names @ n in - let call = apply_to all_names (mkConst depth) call in - let t = apply_to names (mkConst depth) t in - (t,all_names), (names, mkAppC C.pic [Lam call]) + let call = apply_to all_names (Constants.mkConst depth) call in + let t = apply_to names (Constants.mkConst depth) t in + (t,all_names), (names, mkAppC C.pic [Stack.mkLam call]) ) (t,[]) sp in - sp, [Lam t] + sp, [Stack.mkLam t] | (UVar _ | AppUVar _) -> error ~loc "Stack term contains UVar" - | (Arg _ | AppArg _) -> assert false + | (XArg _ | XAppArg _) -> assert false + | (App _ | Cons _ | Lam _ | Builtin _) -> assert false and spaux1 ctx t = let spills, ts = spaux ctx t in @@ -1389,28 +1355,29 @@ let stack_term_of_preterm ~depth:arg_lvl { term = t; amap = { c2i } } = | Const c when C.Map.mem c c2i -> let argno = C.Map.find c c2i in R.mkAppArg argno arg_lvl [] - | Const c -> mkConst c - | App(c, x, xs) when C.Map.mem c c2i -> + | Const c -> Constants.mkConst c + | XApp(c, x, xs) when C.Map.mem c c2i -> let argno = C.Map.find c c2i in R.mkAppArg argno arg_lvl (List.map stack_term_of_preterm (x::xs)) - | App(c, x, xs) as app -> + | XApp(c, x, xs) as app -> let x1 = stack_term_of_preterm x in - let xs1 = smart_map stack_term_of_preterm xs in - if x1 == x && xs1 == xs then app else App(c, x1, xs1) - | Lam t as x -> + let xs1 = Util.smart_map stack_term_of_preterm xs in + if x1 == x && xs1 == xs then app else Stack.mkApp c x1 xs1 + | XLam t as x -> let t1 = stack_term_of_preterm t in - if t1 == t then x else Lam t1 + if t1 == t then x else Stack.mkLam t1 | CData _ as x -> x - | Builtin(c, args) as x -> - let args1 = smart_map stack_term_of_preterm args in - if args1 == args then x else Builtin(c, args1) - | UVar _ | AppUVar _ | Arg _ | AppArg _ -> assert false + | XBuiltin(c, args) as x -> + let args1 = Util.smart_map stack_term_of_preterm args in + if args1 == args then x else Stack.mkBuiltin c args1 | Nil as x -> x - | Discard as x -> x - | Cons(hd, tl) as x -> + | XDiscard () as x -> x + | XCons(hd, tl) as x -> let hd1 = stack_term_of_preterm hd in let tl1 = stack_term_of_preterm tl in - if hd == hd1 && tl == tl1 then x else Cons(hd1,tl1) + if hd == hd1 && tl == tl1 then x else Stack.mkCons hd1 tl1 + | (UVar _ | AppUVar _ | XArg _ | XAppArg _ + | App _ | Lam _ | Cons _ | Builtin _) -> assert false in stack_term_of_preterm t ;; @@ -1667,44 +1634,44 @@ let clausec = C.from_stringc "clause" let mkQApp ~on_type l = let c = if on_type then tappc else appc in - App(c,R.list_to_lp_list l,[]) + Heap.mkApp c (R.list_to_lp_list l) [] let mkQCon ~on_type ?(amap=empty_amap) c = - try mkConst (C.Map.find c amap.c2i) + try Constants.mkConst (C.Map.find c amap.c2i) with Not_found -> let a = if on_type then tconstc else constc in - if c < 0 then App(a,Data.C.of_string (C.show c),[]) - else mkConst (c + amap.nargs) + if c < 0 then Heap.mkApp a (Data.C.of_string (C.show c)) [] + else Constants.mkConst (c + amap.nargs) let quote_preterm ?(on_type=false) { term; amap } = let mkQApp = mkQApp ~on_type in let mkQCon = mkQCon ~on_type ~amap in let rec aux depth term = match term with | Const n when on_type && C.show n = "string" -> - App(C.ctypec, Data.C.of_string "string",[]) + Heap.mkApp C.ctypec (Data.C.of_string "string") [] | Const n when on_type && C.show n = "int" -> - App(C.ctypec, Data.C.of_string "int",[]) + Heap.mkApp C.ctypec (Data.C.of_string "int") [] | Const n when on_type && C.show n = "float" -> - App(C.ctypec, Data.C.of_string "float",[]) + Heap.mkApp C.ctypec (Data.C.of_string "float") [] | App(c,CData s,[]) when on_type && c == C.ctypec && Data.C.is_string s -> term | App(c,s,[t]) when on_type && c == C.arrowc -> - App(arrowc,aux depth s,[aux depth t]) + Heap.mkApp arrowc (aux depth s) [aux depth t] | Const n when on_type && C.show n = "prop" -> term | Const n -> mkQCon n - | Builtin(c,[]) -> mkQCon c - | Lam x -> App(lamc,Lam (aux (depth+1) x),[]) - | App(c,x,xs) -> + | XBuiltin(c,[]) -> mkQCon c + | XLam x -> Heap.mkApp lamc (Heap.mkLam (aux (depth+1) x)) [] + | XApp(c,x,xs) -> mkQApp (mkQCon c :: List.(map (aux depth) (x :: xs))) - | Builtin(c,args) -> mkQApp (mkQCon c :: List.map (aux depth) args) + | XBuiltin(c,args) -> mkQApp (mkQCon c :: List.map (aux depth) args) (* | Arg(id,0) -> mkConst id | Arg(id,argno) -> mkQApp (mkConst id :: C.mkinterval vars argno 0) | AppArg(id,xs) -> mkQApp (mkConst id :: List.map (aux depth) xs) *) - | Arg _ | AppArg _ -> assert false + | XArg _ | XAppArg _ -> assert false (* | UVar ({ contents = g }, from, args) when g != C.dummy -> @@ -1713,11 +1680,12 @@ let quote_preterm ?(on_type=false) { term; amap } = aux depth (deref_appuv ~from ~to_:depth args t) *) | UVar _ | AppUVar _ -> assert false + | (App _ | Lam _ | Builtin _ | Cons _) -> assert false - | CData _ as x -> App(cdatac,x,[]) - | Cons(hd,tl) -> mkQApp [mkQCon C.consc; aux depth hd; aux depth tl] + | CData _ as x -> Heap.mkApp cdatac x [] + | XCons(hd,tl) -> mkQApp [mkQCon C.consc; aux depth hd; aux depth tl] | Nil -> mkQCon C.nilc - | Discard -> mkQCon discardc + | XDiscard () -> mkQCon discardc in aux amap.nargs term @@ -1725,7 +1693,7 @@ let quote_preterm ?(on_type=false) { term; amap } = let close_w_binder binder t { nargs } = let rec close = function | 0 -> t - | n -> App(binder,Lam (close (n-1)),[]) in + | n -> Heap.mkApp binder (Heap.mkLam (close (n-1))) [] in close nargs let sorted_names_of_argmap argmap = @@ -1744,16 +1712,17 @@ let quote_clause { Ast.Clause.loc; attributes = { Assembled.id }; body } = let clloc = quote_loc ?id loc in let qt = close_w_binder argc (quote_preterm body) body.amap in let names = sorted_names_of_argmap body.amap in - App(clausec,CData clloc,[R.list_to_lp_list names; qt]) + Heap.mkApp clausec (Pure.mkCData clloc) [R.list_to_lp_list names; qt] ;; let quote_syntax { WithMain.clauses; query } = let names = sorted_names_of_argmap query.amap in let clist = List.map quote_clause clauses in let q = - App(clausec,CData (quote_loc ~id:"query" query.loc), + Heap.mkApp clausec + (Pure.mkCData (quote_loc ~id:"query" query.loc)) [R.list_to_lp_list names; - close_w_binder argc (quote_preterm ~on_type:false query) query.amap]) in + close_w_binder argc (quote_preterm ~on_type:false query) query.amap] in clist, q let default_checker () = @@ -1768,9 +1737,9 @@ let static_check header let p,q = quote_syntax q in let tlist = R.list_to_lp_list (List.map (fun { Structured.decl = { tname; ttype } } -> - App(C.from_stringc "`:",mkQCon ~on_type:false tname, + Heap.mkApp (C.from_stringc "`:") (mkQCon ~on_type:false tname) [close_w_binder forallc (quote_preterm ~on_type:true ttype) - ttype.amap])) + ttype.amap]) types) in let checker = program_of_ast @@ -1780,7 +1749,7 @@ let static_check header let query = query_of_term checker (fun ~depth state -> assert(depth=0); - state, (loc,App(C.from_stringc "check",R.list_to_lp_list p,[q;tlist]))) in + state, (loc,Heap.mkApp(C.from_stringc "check") (R.list_to_lp_list p) [q;tlist])) in let executable = executable_of_query query in exec executable <> Failure ;; diff --git a/src/data.ml b/src/data.ml index 08d027981..23505f0a8 100644 --- a/src/data.ml +++ b/src/data.ml @@ -35,7 +35,230 @@ open Util * *) -module Term = struct +module Term : sig + +type constant = int +[@@deriving show, eq] + +val id_term : UUID.t +type term = private + + (* Pure terms, can live both on the heap and on the stack *) + | Const of constant + | CData of CData.t + | Nil + + (* Heap *) + | Lam of term + | App of constant * term * term list + | Builtin of constant * term list + | Cons of term * term + | UVar of uvar_body * (*depth:*)int * (*argsno:*)int + | AppUVar of uvar_body * (*depth:*)int * term list + + (* Stack: these constructors are later hidden via an Obj.magic *) + | XLam of term + | XApp of constant * term * term list + | XArg of (*id:*)int * (*argsno:*)int + | XAppArg of (*id*)int * term list + | XCons of term * term + | XBuiltin of constant * term list + | XDiscard of unit (* we need an argument, or this constructor goes up *) +and uvar_body = { + mutable contents : term; + mutable rest : stuck_goal list; +} +and stuck_goal = { + mutable blockers : blockers; + kind : stuck_goal_kind; +} +and blockers = uvar_body list +and stuck_goal_kind = + | Constraint of constraint_def + | Unification of unification_def +and unification_def = { + adepth : int; + env : term array; + bdepth : int; + a : term; + b : term; + matching: bool; +} +and constraint_def = { + cdepth : int; + prog : prolog_prog [@equal fun _ _ -> true] + [@printer (fun fmt _ -> Fmt.fprintf fmt "")]; + context : clause_src list; + conclusion : term; +} +and clause_src = { hdepth : int; hsrc : term } +and prolog_prog = { + src : clause_src list; (* hypothetical context in original form, for CHR *) + index : index; +} +and index = second_lvl_idx Ptmap.t +and second_lvl_idx = +| TwoLevelIndex of { + mode : mode; + argno : int; + all_clauses : clause list; (* when the query is flexible *) + flex_arg_clauses : clause list; (* when the query is rigid but arg_id ha nothing *) + arg_idx : clause list Ptmap.t; (* when the query is rigid (includes in each binding flex_arg_clauses) *) + } +| BitHash of { + mode : mode; + args : int list; + time : int; (* time is used to recover the total order *) + args_idx : (clause * int) list Ptmap.t; (* clause, insertion time *) + } +and clause = { + depth : int; + args : term list; + hyps : term list; + vars : int; + mode : mode; (* CACHE to avoid allocation in get_clause *) +} +and mode = bool list (* true=input, false=output *) +[@@deriving show, eq] + +module Pure : sig + +val mkNil : term [@@inline] +val mkCData : CData.t -> term [@@inline] +val mkConst : constant -> term [@@inline] + +end + +module Heap : sig + +val mkLam : term -> term [@@inline] +val mkApp : constant -> term -> term list -> term [@@inline] +val mkCons : term -> term -> term [@@inline] +val mkBuiltin : constant -> term list -> term [@@inline] +val mkUVar : uvar_body -> int -> int -> term [@@inline] +val mkAppUVar : uvar_body -> int -> term list -> term [@@inline] + +end + +module Stack : sig + +val mkLam : term -> term [@@inline] +val mkApp : constant -> term -> term list -> term [@@inline] +val mkCons : term -> term -> term [@@inline] +val mkDiscard : unit -> term [@@inline] +val mkBuiltin : constant -> term list -> term [@@inline] +val mkArg : int -> int -> term [@@inline] +val mkAppArg : int -> term list -> term [@@inline] + +end + +val mkAppL : constant -> term list -> term [@@inline] +val mkAppS : string -> term -> term list -> term [@@inline] +val mkAppSL : string -> term list -> term [@@inline] + +val smart_map : (constant -> constant) -> term -> term + +module C : sig + + val int : int CData.cdata + val is_int : CData.t -> bool + val to_int : CData.t -> int + val of_int : int -> term + + val float : float CData.cdata + val is_float : CData.t -> bool + val to_float : CData.t -> float + val of_float : float -> term + + val string : string CData.cdata + val is_string : CData.t -> bool + val to_string : CData.t -> string + val of_string : string -> term + + val loc : Util.Loc.t CData.cdata + val is_loc : CData.t -> bool + val to_loc : CData.t -> Util.Loc.t + val of_loc : Util.Loc.t -> term + +end + +val destConst : term -> constant + +(* Our ref data type: creation and dereference. Assignment is defined + After the constraint store, since assigning may wake up some constraints *) +val oref : term -> uvar_body [@@inline] +val (!!) : uvar_body -> term [@@inline] +val pp_oref : (UUID.t * Obj.t) Util.extensible_printer + +(* Arg/AppArg point to environments, here the empty one *) +type env = term array +val empty_env : env + +(* - negative constants are global names + - constants are hashconsed (terms) + - we use special constants to represent !, pi, sigma *) +module Constants : sig + + val funct_of_ast : F.t -> constant * term + val mkConst : constant -> term + val show : constant -> string + val pp : Fmt.formatter -> constant -> unit + val fresh : unit -> constant * term + val from_string : string -> term + val from_stringc : string -> constant + + (* To keep the type of terms small, we use special constants for !, =, pi.. *) + (* {{{ *) + val cutc : constant + val truec : term + val andc : constant + val andt : term + val andc2 : constant + val orc : constant + val implc : constant + val rimplc : constant + val rimpl : term + val pic : constant + val pi : term + val sigmac : constant + val eqc : constant + val rulec : constant + val cons : term + val consc : constant + val nil : term + val nilc : constant + val entailsc : constant + val nablac : constant + val asc : constant + val arrowc : constant + val uvarc : constant + + val ctypec : constant + val prop : term + val variadic : constant + val any : term + + val spillc : constant + + val declare_constraintc : constant + val print_constraintsc : constant + (* }}} *) + + (* Value for unassigned UVar/Arg *) + val dummy : term + + type t = constant + val compare : t -> t -> int + + module Map : Map.S with type key = t + module Set : Set.S with type elt = t + + (* mkinterval d n 0 = [d; ...; d+n-1] *) + val mkinterval : int -> int -> int -> term list + +end + +end = struct (* Used by pretty printers, to be later instantiated in module Constants *) let pp_const = mk_extensible_printer () @@ -48,23 +271,28 @@ let pp_oref = mk_extensible_printer () let id_term = UUID.make () type term = - (* Pure terms *) + + (* Pure terms, can live both on the heap and on the stack *) | Const of constant + | CData of CData.t + | Nil + + (* Heap *) | Lam of term | App of constant * term * term list - (* Optimizations *) - | Cons of term * term - | Nil - | Discard - (* FFI *) | Builtin of constant * term list - | CData of CData.t - (* Heap terms: unif variables in the query *) + | Cons of term * term | UVar of uvar_body * (*depth:*)int * (*argsno:*)int | AppUVar of uvar_body * (*depth:*)int * term list - (* Clause terms: unif variables used in clauses *) - | Arg of (*id:*)int * (*argsno:*)int - | AppArg of (*id*)int * term list + + (* Stack: these constructors are later hidden via an Obj.magic *) + | XLam of term + | XApp of constant * term * term list + | XArg of (*id:*)int * (*argsno:*)int + | XAppArg of (*id*)int * term list + | XCons of term * term + | XBuiltin of constant * term list + | XDiscard of unit (* we need an argument, or this constructor goes up *) and uvar_body = { mutable contents : term [@printer (pp_extensible_any ~id:id_term pp_oref)]; mutable rest : stuck_goal list [@printer fun _ _ -> ()] @@ -123,22 +351,13 @@ and clause = { and mode = bool list (* true=input, false=output *) [@@deriving show, eq] -type indexing = - | MapOn of int - | Hash of int list -[@@deriving show] +module Pure = struct + +let mkNil = Nil [@@inlined] +let mkCData c = CData c [@@inlined] +let mkConst x = Const x [@@inlined] -let mkLam x = Lam x [@@inline] -let mkApp c x xs = App(c,x,xs) [@@inline] -let mkCons hd tl = Cons(hd,tl) [@@inline] -let mkNil = Nil -let mkDiscard = Discard -let mkBuiltin c args = Builtin(c,args) [@@inline] -let mkCData c = CData c [@@inline] -let mkUVar r d ano = UVar(r,d,ano) [@@inline] -let mkAppUVar r d args = AppUVar(r,d,args) [@@inline] -let mkArg i ano = Arg(i,ano) [@@inline] -let mkAppArg i args = AppArg(i,args) [@@inline] +end module C = struct @@ -171,8 +390,8 @@ let destConst = function Const x -> x | _ -> assert false (* Our ref data type: creation and dereference. Assignment is defined After the constraint store, since assigning may wake up some constraints *) -let oref x = { contents = x; rest = [] } -let (!!) { contents = x } = x +let oref x = { contents = x; rest = [] } [@@inline] +let (!!) { contents = x } = x [@@inline] (* Arg/AppArg point to environments, here the empty one *) type env = term array @@ -270,7 +489,7 @@ let mkConst x = Hashtbl.add c2s x ("c" ^ string_of_int x); Hashtbl.add c2t x xx; xx - [@@inline] + [@@inlined] let show n = try Hashtbl.find c2s n @@ -346,16 +565,93 @@ let rec mkinterval depth argsno n = end (* }}} *) -let mkConst x = Constants.mkConst x [@@inline] + +module Heap = struct + +let mkLam x = Lam x [@@inlined] +let mkApp c x xs = App(c,x,xs) [@@inlined] +let mkCons hd tl = Cons(hd,tl) [@@inlined] +let mkBuiltin c args = Builtin(c,args) [@@inlined] +let mkUVar r d ano = UVar(r,d,ano) [@@inlined] +let mkAppUVar r d args = AppUVar(r,d,args) [@@inlined] + +end + +module Stack = struct + +let mkLam x = XLam x [@@inlined] +let mkApp c x xs = XApp(c,x,xs) [@@inlined] +let mkCons hd tl = XCons(hd,tl) [@@inlined] +let mkDiscard () = XDiscard () +let mkBuiltin c args = XBuiltin(c,args) [@@inlined] +let mkArg i ano = XArg(i,ano) [@@inlined] +let mkAppArg i args = XAppArg(i,args) [@@inlined] + +end + let mkAppL c = function - | [] -> mkConst c - | x::xs -> mkApp c x xs [@@inline] -let mkAppS s x args = mkApp (Constants.from_stringc s) x args [@@inline] + | [] -> Constants.mkConst c + | x::xs -> Heap.mkApp c x xs [@@inline] +let mkAppS s x args = Heap.mkApp (Constants.from_stringc s) x args [@@inline] let mkAppSL s args = mkAppL (Constants.from_stringc s) args [@@inline] +let smart_map f t = + let rec aux = function + | Const c as x -> + let c1 = f c in + if c == c1 then x else Constants.mkConst c1 + | Lam t as x -> + let t1 = aux t in + if t == t1 then x else Heap.mkLam t1 + | XLam t as x -> + let t1 = aux t in + if t == t1 then x else Stack.mkLam t1 + | XAppArg(i,ts) as x -> + let ts1 = smart_map aux ts in + if ts == ts1 then x else Stack.mkAppArg i ts1 + | AppUVar(r,lvl,ts) as x -> + assert(!!r == Constants.dummy); + let ts1 = smart_map aux ts in + if ts == ts1 then x else Heap.mkAppUVar r lvl ts1 + | Builtin(c,ts) as x -> + let ts1 = smart_map aux ts in + if ts == ts1 then x else Heap.mkBuiltin (f c) ts1 + | XBuiltin(c,ts) as x -> + let ts1 = smart_map aux ts in + if ts == ts1 then x else Stack.mkBuiltin (f c) ts1 + | App(c,t,ts) as x -> + let c1 = f c in + let t1 = aux t in + let ts1 = smart_map aux ts in + if c == c1 && t == t1 && ts == ts1 then x else Heap.mkApp c1 t1 ts1 + | XApp(c,t,ts) as x -> + let c1 = f c in + let t1 = aux t in + let ts1 = smart_map aux ts in + if c == c1 && t == t1 && ts == ts1 then x else Stack.mkApp c1 t1 ts1 + | Cons(hd,tl) as x -> + let hd1 = aux hd in + let tl1 = aux tl in + if hd == hd1 && tl == tl1 then x else Heap.mkCons hd1 tl1 + | XCons(hd,tl) as x -> + let hd1 = aux hd in + let tl1 = aux tl in + if hd == hd1 && tl == tl1 then x else Stack.mkCons hd1 tl1 + | UVar(r,_,_) as x -> + assert(!!r == Constants.dummy); + x + | (XArg _ | CData _ | Nil | XDiscard _) as x -> x + in + aux t + end include Term +type indexing = + | MapOn of int + | Hash of int list +[@@deriving show] + (* Object oriented state: borns at compilation time and survives as run time *) module State : sig @@ -795,8 +1091,8 @@ type 't compiled_constructor = type 't compiled_adt = ('t compiled_constructor) Constants.Map.t let buildk kname = function -| [] -> mkConst kname -| x :: xs -> mkApp kname x xs +| [] -> Constants.mkConst kname +| x :: xs -> Heap.mkApp kname x xs let rec readback_args : type a m t. look:(depth:int -> term -> term) -> @@ -832,10 +1128,6 @@ and readback : type t. | (UVar _ | AppUVar _) -> let CK(args,read,_) = Constants.Map.find (Constants.from_stringc "uvar") adt in readback_args ~look ty ~depth hyps constraints state [] t args read [t] - | Discard -> - let CK(args,read,_) = Constants.Map.find (Constants.from_stringc "uvar") adt in - let state, k = alloc ~lvl:depth state in - readback_args ~look ty ~depth hyps constraints state [] t args read [mkUnifVar k ~args:[] state] | _ -> raise (Conversion.TypeErr(ty,depth,t)) with Not_found -> raise (Conversion.TypeErr(ty,depth,t)) diff --git a/src/runtime.ml b/src/runtime.ml index d3ec5b942..eec9114aa 100644 --- a/src/runtime.ml +++ b/src/runtime.ml @@ -90,11 +90,11 @@ let xppterm ~nice ?(min_prec=min_prec) depth0 names argsdepth env f t = | AppUVar (r,vardepth,terms) when !!r != C.dummy -> flat_cons_to_list depth acc (!do_app_deref ~from:vardepth ~to_:depth terms !!r) - | Cons (x,y) -> flat_cons_to_list depth (x::acc) y + | Cons (x,y) | XCons (x,y) -> flat_cons_to_list depth (x::acc) y | _ -> List.rev acc, t and is_lambda depth = function - Lam _ -> true + | Lam _ | XLam _ -> true | UVar (r,vardepth,terms) when !!r != C.dummy -> is_lambda depth (!do_deref ~from:vardepth ~to_:depth terms !!r) | AppUVar (r,vardepth,terms) when !!r != C.dummy -> @@ -103,7 +103,7 @@ let xppterm ~nice ?(min_prec=min_prec) depth0 names argsdepth env f t = and aux_last prec depth f t = if nice then begin match t with - Lam _ -> aux min_prec depth f t + Lam _ | XLam _ -> aux min_prec depth f t | UVar (r,vardepth,terms) when !!r != C.dummy -> aux_last prec depth f (!do_deref ~from:vardepth ~to_:depth terms !!r) | AppUVar (r,vardepth,terms) when !!r != C.dummy -> @@ -117,17 +117,17 @@ let xppterm ~nice ?(min_prec=min_prec) depth0 names argsdepth env f t = (Fmt.fprintf f "(" ; h () ; Fmt.fprintf f ")") else h () in match t with - | (Cons _ | Nil) -> + | (Cons _ | Nil) | XCons _ -> let prefix,last = flat_cons_to_list depth [] t in Fmt.fprintf f "[" ; pplist ~boxed:true (aux Parser.list_element_prec depth) ", " f prefix ; - if last != Nil then begin + if last != Pure.mkNil then begin Fmt.fprintf f " | " ; aux prec 1 f last end; Fmt.fprintf f "]" | Const s -> ppconstant f s - | App (hd,x,xs) -> + | App (hd,x,xs) | XApp (hd,x,xs) -> (try let assoc,hdlvl = Parser.precedence_of (F.from_string (C.show hd)) in @@ -165,7 +165,7 @@ let xppterm ~nice ?(min_prec=min_prec) depth0 names argsdepth env f t = pplist (aux inf_prec depth) ~pplastelem:(aux_last inf_prec depth) ", " f (x::xs) else pp_app f ppconstant (aux inf_prec depth) ~pplastarg:(aux_last inf_prec depth) (hd,x::xs))) - | Builtin (hd,xs) -> + | Builtin (hd,xs) | XBuiltin(hd,xs) -> with_parens appl_prec (fun _ -> pp_app f ppconstant (aux inf_prec depth) ~pplastarg:(aux_last inf_prec depth) (hd,xs)) @@ -190,21 +190,21 @@ let xppterm ~nice ?(min_prec=min_prec) depth0 names argsdepth env f t = with_parens appl_prec (fun _ -> pp_app f (pp_uvar inf_prec depth vardepth 0) (aux inf_prec depth) ~pplastarg:(aux_last inf_prec depth) (r,terms)) - | Arg (n,argsno) -> + | XArg (n,argsno) -> let args = List.map destConst (C.mkinterval argsdepth argsno 0) in with_parens ~test:(args <> []) appl_prec (fun _ -> pp_app f (pp_arg prec depth) ppconstant (n,args)) - | AppArg (v,terms) -> + | XAppArg (v,terms) -> with_parens appl_prec (fun _ -> pp_app f (pp_arg inf_prec depth) (aux inf_prec depth) ~pplastarg:(aux_last inf_prec depth) (v,terms)) - | Lam t -> + | Lam t | XLam t -> with_parens lam_prec (fun _ -> - let c = mkConst depth in + let c = Constants.mkConst depth in Fmt.fprintf f "%a \\@ %a" (aux inf_prec depth) c (aux min_prec (depth+1)) t) | CData d -> CData.pp f d - | Discard -> Fmt.fprintf f "_" + | XDiscard () -> Fmt.fprintf f "_" in try aux min_prec depth0 f t with e -> Fmt.fprintf f "EXN PRINTING: %s" (Printexc.to_string e) ;; @@ -447,7 +447,7 @@ let print = pp_ctx pdiff (pp_goal depth) g (pplist (uppterm 0 [] 0 empty_env) ", ") - (List.map (fun r -> UVar(r,0,0)) blockers) + (List.map (fun r -> Heap.mkUVar r 0 0) blockers) ) " " let pp_stuck_goal fmt { kind; blockers } = match kind with @@ -457,7 +457,7 @@ let pp_stuck_goal fmt { kind; blockers } = match kind with ad (uppterm ad [] 0 empty_env) a bd (uppterm ad [] ad e) b (pplist ~boxed:false (uppterm 0 [] 0 empty_env) ", ") - (List.map (fun r -> UVar(r,0,0)) blockers) + (List.map (fun r -> Heap.mkUVar r 0 0) blockers) | Constraint c -> print fmt [c,blockers] end (* }}} *) @@ -534,44 +534,59 @@ end = struct (* {{{ ************** move/hmove/deref_* ******************** *) -exception NotInTheFragment (* in_fragment n [n;...;n+m-1] = m it must be called either on heap terms or on stack terms whose Args are non instantiated *) -let rec in_fragment expected = - function - [] -> 0 - | Const c::tl when c = expected -> 1 + in_fragment (expected+1) tl - | UVar ({ contents = t} ,_,_)::tl -> (* XXX *) - in_fragment expected (t :: tl) -(* Invariant not true anymore, since we may not deref aggressively - to avoid occur-check - | UVar (r,_,_)::_ - | AppUVar (r,_,_)::_ when !!r != C.dummy -> - anomaly "non dereferenced terms in in_fragment" -*) - | _ -> raise NotInTheFragment +let rec uvar_in_fragment r lvl ol expected l cur = + match l with + | [] -> Heap.mkUVar r lvl cur + | Const c::tl when c = expected -> uvar_in_fragment r lvl ol (expected+1) tl (succ cur) + | UVar ({ contents = t} ,_,_)::tl -> (* Approx, we don't deref if we are avoid OC *) + uvar_in_fragment r lvl ol expected (t :: tl) cur + | _ -> Heap.mkAppUVar r lvl ol +[@@inlined] + +let rec uvar_in_fragment_beta r lvl ano ol expected l cur = + match l with + | [] -> Heap.mkUVar r lvl (ano+cur) + | Const c::tl when c = expected -> uvar_in_fragment_beta r lvl ano ol (expected+1) tl (succ cur) + | UVar ({ contents = t} ,_,_)::tl -> (* Approx, we don't deref if we are avoid OC *) + uvar_in_fragment_beta r lvl ano ol expected (t :: tl) cur + | _ -> + let nl = C.mkinterval lvl ano 0 in + Heap.mkAppUVar r lvl (nl@ol) +[@@inlined] + +let rec arg_in_fragment r ol expected l cur = + match l with + | [] -> Stack.mkArg r cur + | Const c::tl when c = expected -> arg_in_fragment r ol (expected+1) tl (succ cur) + | UVar ({ contents = t} ,_,_)::tl -> (* Approx, we don't deref if we are avoid OC *) + arg_in_fragment r ol expected (t :: tl) cur + | _ -> Stack.mkAppArg r ol +[@@inlined] + exception NonMetaClosed let deterministic_restriction e ~args_safe t = let rec aux = function - Lam f -> aux f - | App (_,t,l) -> aux t; List.iter aux l - | Cons (x,xs) -> aux x; aux xs - | Builtin (_,l) -> List.iter aux l + | Lam f | XLam f -> aux f + | App (_,t,l) | XApp (_,t,l) -> aux t; List.iter aux l + | Cons (x,xs) | XCons (x,xs) -> aux x; aux xs + | Builtin (_,l) | XBuiltin (_,l) -> List.iter aux l | UVar (r,_,_) | AppUVar (r,_,_) when !!r == C.dummy -> raise NonMetaClosed | UVar (r,_,_) -> aux !!r | AppUVar (r,_,l) -> aux !!r ; List.iter aux l - | Arg (i,_) when e.(i) == C.dummy && not args_safe -> raise NonMetaClosed - | AppArg (i,_) when e.(i) == C.dummy -> raise NonMetaClosed - | Arg (i,_) -> if e.(i) != C.dummy then aux e.(i) - | AppArg (i,l) -> aux e.(i) ; List.iter aux l + | XArg (i,_) when e.(i) == C.dummy && not args_safe -> raise NonMetaClosed + | XAppArg (i,_) when e.(i) == C.dummy -> raise NonMetaClosed + | XArg (i,_) -> if e.(i) != C.dummy then aux e.(i) + | XAppArg (i,l) -> aux e.(i) ; List.iter aux l | Const _ | Nil - | Discard + | XDiscard () | CData _ -> () in try aux t ; true @@ -585,18 +600,16 @@ let occurr_check r1 r2 = | Some r1 -> if r1 == r2 then raise RestrictionFailure let rec make_lambdas destdepth args = - if args = 0 then let x = UVar(oref C.dummy,destdepth,0) in x,x - else let x,y = make_lambdas (destdepth+1) (args-1) in Lam x, y + if args = 0 then let x = Heap.mkUVar (oref C.dummy) destdepth 0 in x,x + else let x,y = make_lambdas (destdepth+1) (args-1) in Heap.mkLam x, y -let rec mknLam n x = if n = 0 then x else Lam (mknLam (n-1) x) +let rec mknLam n x = if n = 0 then x else Heap.mkLam (mknLam (n-1) x) -let mkAppUVar r lvl l = - try UVar(r,lvl,in_fragment lvl l) - with NotInTheFragment -> AppUVar(r,lvl,l) +let mkAppUVar r lvl l = uvar_in_fragment r lvl l lvl l 0 +[@@inlined] -let mkAppArg i fromdepth xxs' = - try Arg(i,in_fragment fromdepth xxs') - with NotInTheFragment -> AppArg (i,xxs') +let mkAppArg i fromdepth xxs' = arg_in_fragment i xxs' fromdepth xxs' 0 +[@@inlined] (* move performs at once: 1) refreshing of the arguments into variables (heapifycation) @@ -708,29 +721,29 @@ let rec move ~adepth:argsdepth e ?avoid ?(depth=0) ~from ~to_ t = match x with | Const c -> if delta == 0 then x else (* optimization *) - if c >= from then mkConst (c - delta) else (* locally bound *) + if c >= from then Constants.mkConst (c - delta) else (* locally bound *) if c < to_ then x else (* constant *) raise RestrictionFailure | Lam f -> let f' = maux e (depth+1) f in - if f == f' then x else Lam f' + if f == f' then x else mkLam f' | App (c,t,l) when delta == 0 || c < from && c < to_ -> let t' = maux e depth t in let l' = smart_map (maux e depth) l in - if t == t' && l == l' then x else App (c,t',l') + if t == t' && l == l' then x else mkApp c t' l' | App (c,t,l) when c >= from -> - App(c-delta, maux e depth t, smart_map (maux e depth) l) + mkApp (c-delta) (maux e depth t) (smart_map (maux e depth) l) | App _ -> raise RestrictionFailure | Builtin (c,l) -> let l' = smart_map (maux e depth) l in - if l == l' then x else Builtin (c,l') + if l == l' then x else mkBuiltin c l' | CData _ -> x | Cons(hd,tl) -> let hd' = maux e depth hd in let tl' = maux e depth tl in - if hd == hd' && tl == tl' then x else Cons(hd',tl') + if hd == hd' && tl == tl' then x else mkCons hd' tl' | Nil -> x - | Discard -> x + | XDiscard () -> x (* fast path with no deref... *) | UVar _ when delta == 0 && avoid == None -> x @@ -755,9 +768,9 @@ let rec move ~adepth:argsdepth e ?avoid ?(depth=0) ~from ~to_ t = | Arg (i, args) -> let to_ = min argsdepth to_ in let r = oref C.dummy in - let v = UVar(r,to_,0) in + let v = mkUVar r to_ 0 in e.(i) <- v; - if args == 0 then v else UVar(r,to_,args) + if args == 0 then v else mkUVar r to_ args | AppArg(i, args) when List.for_all (deterministic_restriction e ~args_safe:(argsdepth=to_)) args -> @@ -767,7 +780,7 @@ let rec move ~adepth:argsdepth e ?avoid ?(depth=0) ~from ~to_ t = with RestrictionFailure -> anomaly "TODO: implement deterministic restriction" in let r = oref C.dummy in - let v = UVar(r,to_,0) in + let v = mkUVar r to_ 0 in e.(i) <- v; mkAppUVar r to_ args | AppArg _ -> @@ -813,14 +826,14 @@ let rec move ~adepth:argsdepth e ?avoid ?(depth=0) ~from ~to_ t = with RestrictionFailure -> anomaly "impossible, delta < 0" in mkAppUVar r vardepth args else if delta == 0 then - AppUVar (r,vardepth,List.map (maux e depth) args) + mkAppUVar r vardepth (List.map (maux e depth) args) else if List.for_all (deterministic_restriction e ~args_safe:(argsdepth=to_)) args then (* TODO: this branch is to be reviewed/tested throughly, unless Enrico is now confident with it *) let r,vardepth = if vardepth <= to_ then r,vardepth else begin - let newvar = UVar(oref C.dummy,to_,0) in + let newvar = mkUVar (oref C.dummy) to_ 0 in r @:= newvar; r,vardepth (*CSC: XXX why vardepth and not to_ ? *) end in @@ -871,7 +884,7 @@ and decrease_depth r ~from ~to_ argsno = else let newr = oref C.dummy in let newargsno = argsno+from-to_ in - let newvar = UVar(newr,to_,from-to_) in + let newvar = mkUVar newr to_ (from - to_) in r @:= newvar; newr,to_,newargsno @@ -910,15 +923,15 @@ and subst fromdepth ts t = let t = hmove ~from:fromdepth ~to_:(depth-len) t in beta (depth-len) [] t xxs' else if c < fromdepth then - if x==x' && xs==xs' then orig else App(c,x',xs') - else App(c-len,x',xs') + if x==x' && xs==xs' then orig else mkApp c x' xs' + else mkApp (c - len) x' xs' | Builtin(c,xs) as orig -> let xs' = List.map (aux depth) xs in - if xs==xs' then orig else Builtin(c,xs') + if xs==xs' then orig else mkBuiltin c xs' | Cons(hd,tl) as orig -> let hd' = aux depth hd in let tl' = aux depth tl in - if hd == hd' && tl == tl' then orig else Cons(hd',tl') + if hd == hd' && tl == tl' then orig else mkCons hd' tl' | Nil -> tt | Discard -> tt | UVar({contents=g},vardepth,argsno) when g != C.dummy -> @@ -939,7 +952,7 @@ and subst fromdepth ts t = let args0 = C.mkinterval vardepth argsno 0 in let args = List.map (aux depth) (args0@args) in mkAppUVar r vardepth args - | Lam t -> Lam (aux (depth+1) t) + | Lam t -> mkLam (aux (depth+1) t) | CData _ as x -> x end] in aux fromdepthlen t @@ -964,17 +977,13 @@ and beta depth sub t args = | [] -> t' | ahd::atl -> match t' with - | Const c -> App (c,ahd,atl) + | Const c -> mkApp c ahd atl | Arg _ | AppArg _ -> anomaly "beta takes only heap terms" - | App (c,arg,args1) -> App (c,arg,args1@args) - | Builtin (c,args1) -> Builtin (c,args1@args) - | UVar (r,n,m) -> begin - try UVar(r,n,m + in_fragment (n+m) args) - with NotInTheFragment -> - let args1 = C.mkinterval n m 0 in - AppUVar (r,n,args1@args) end - | AppUVar (r,depth,args1) -> AppUVar (r,depth,args1@args) + | App (c,arg,args1) -> mkApp c arg (args1@args) + | Builtin (c,args1) -> mkBuiltin c (args1@args) + | UVar (r,n,m) -> uvar_in_fragment_beta r n m args (n+m) args 0 + | AppUVar (r,depth,args1) -> mkAppUVar r depth (args1@args) | Lam _ -> anomaly "beta: some args and some lambdas" | CData x -> type_error (Printf.sprintf "beta: '%s'" (CData.show x)) | Nil -> type_error "beta: Nil" @@ -1025,26 +1034,26 @@ and deref_uv ?avoid ~from ~to_ args t = | Lam _ -> anomaly "eat_args went crazy" | Const c -> let args = C.mkinterval (from+1) (args'-1) 0 in - App (c,mkConst from, args) + mkApp c (mkConst from) args | App (c,arg,args2) -> let args = C.mkinterval from args' 0 in - App (c,arg,args2 @ args) + mkApp c arg (args2 @ args) | Builtin (c,args2) -> let args = C.mkinterval from args' 0 in - Builtin (c,args2 @ args) + mkBuiltin c (args2 @ args) (* TODO: when the UVar/Arg is not C.dummy, we call deref_uv that will call move that will call_deref_uv again. Optimize the path *) | UVar(t,depth,args2) when from = depth+args2 -> - UVar(t,depth,args2+args') + mkUVar t depth (args2+args') | AppUVar (r,depth,args2) -> let args = C.mkinterval from args' 0 in - AppUVar (r,depth,args2 @ args) + mkAppUVar r depth (args2 @ args) | UVar (r,vardepth,argsno) -> let args1 = C.mkinterval vardepth argsno 0 in let args2 = C.mkinterval from args' 0 in let args = args1 @ args2 in - AppUVar (r,vardepth,args) + mkAppUVar r vardepth args | Cons _ | Nil -> type_error "deref_uv: applied list" | Discard -> type_error "deref_uv: applied Discard" | CData _ -> t @@ -1128,7 +1137,7 @@ let is_llam lvl args adepth bdepth depth left e = (pplist (fun fmt (x,n) -> Fmt.fprintf fmt "%d |-> %d" x n) " ") map) res]; res -let rec mknLam n t = if n = 0 then t else mknLam (n-1) (Lam t) +let rec mknLam n t = if n = 0 then t else mknLam (n-1) (mkLam t) (* [bind r args ... t] generates a term \args.t' to be assigned to r. * r is the variable being assigned @@ -1173,13 +1182,13 @@ let bind r gamma l a d delta b left t e = (ppterm a [] b empty_env) t a delta d w b) begin match t with | UVar (r1,_,_) | AppUVar (r1,_,_) when r == r1 -> raise RestrictionFailure - | Const c -> let n = cst c b delta in if n < 0 then mkConst n else Const n - | Lam t -> Lam (bind b delta (w+1) t) - | App (c,t,ts) -> App (cst c b delta, bind b delta w t, List.map (bind b delta w) ts) - | Cons(hd,tl) -> Cons(bind b delta w hd, bind b delta w tl) + | Const c -> let n = cst c b delta in (*if n < 0 then*) mkConst n (*else Const n*) + | Lam t -> mkLam (bind b delta (w+1) t) + | App (c,t,ts) -> mkApp (cst c b delta) (bind b delta w t) (List.map (bind b delta w) ts) + | Cons(hd,tl) -> mkCons (bind b delta w hd) (bind b delta w tl) | Nil -> t | Discard -> t - | Builtin (c, tl) -> Builtin(c, List.map (bind b delta w) tl) + | Builtin (c, tl) -> mkBuiltin c (List.map (bind b delta w) tl) | CData _ -> t (* deref_uv *) | Arg (i,args) when e.(i) != C.dummy -> @@ -1197,28 +1206,28 @@ let bind r gamma l a d delta b left t e = | UVar(r,lvl,0) -> r, lvl, (true, []), [] | UVar(r,lvl,args) -> let r' = oref C.dummy in - let v = UVar(r',lvl+args,0) in + let v = mkUVar r' (lvl+args) 0 in r @:= mknLam args v; r', (lvl+args), (true,[]), [] | AppUVar (r,lvl, orig_args) -> r, lvl, is_llam lvl orig_args a b (d+w) left e, orig_args | Arg (i,0) -> let r = oref C.dummy in - let v = UVar(r,a,0) in + let v = mkUVar r a 0 in e.(i) <- v; r, a, (true,[]), [] | Arg (i,args) -> let r = oref C.dummy in - let v = UVar(r,a,0) in + let v = mkUVar r a 0 in e.(i) <- v; let r' = oref C.dummy in - let v' = UVar(r',a+args,0) in + let v' = mkUVar r' (a+args) 0 in r @:= mknLam args v'; r', a+args, (true, []), [] | AppArg (i,orig_args) -> let is_llam, args = is_llam a orig_args a b (d+w) false e in let r = oref C.dummy in - let v = UVar(r,a,0) in + let v = mkUVar r a 0 in e.(i) <- v; r, a, (is_llam, args), orig_args | _ -> assert false in @@ -1294,7 +1303,7 @@ let bind r gamma l a d delta b left t e = try let v = mknLam new_lams (bind b delta 0 t) in [%spy "assign(HO)" (fun fmt _ -> Fmt.fprintf fmt "%a := %a" - (uppterm gamma [] a e) (UVar(r,gamma,0)) + (uppterm gamma [] a e) (mkUVar r gamma 0) (uppterm gamma [] a e) v) ()]; r @:= v; true @@ -1303,8 +1312,8 @@ let bind r gamma l a d delta b left t e = (* exception Non_linear *) let rec list_to_lp_list = function - | [] -> Nil - | x::xs -> Cons(x,list_to_lp_list xs) + | [] -> mkNil + | x::xs -> mkCons x (list_to_lp_list xs) ;; let delay_hard_unif_problems = Fork.new_local false @@ -1371,20 +1380,20 @@ let rec unif matching depth adepth a bdepth b e = (* UVar introspection (matching) *) | (UVar _ | AppUVar _), Const c when c == C.uvarc && matching -> true | UVar(r,vd,ano), App(c,hd,[]) when c == C.uvarc && matching -> - unif matching depth adepth (UVar(r,vd,ano)) bdepth hd e + unif matching depth adepth a bdepth hd e | AppUVar(r,vd,_), App(c,hd,[]) when c == C.uvarc && matching -> - unif matching depth adepth (UVar(r,vd,0)) bdepth hd e + unif matching depth adepth (mkUVar r vd 0) bdepth hd e | UVar(r,vd,ano), App(c,hd,[arg]) when c == C.uvarc && matching -> let r_exp = oref C.dummy in - let exp = UVar(r_exp,0,0) in - r @:= UVar(r_exp,0,vd); + let exp = mkUVar r_exp 0 0 in + r @:= mkUVar r_exp 0 vd; unif matching depth adepth exp bdepth hd e && let args = list_to_lp_list (C.mkinterval 0 (vd+ano) 0) in unif matching depth adepth args bdepth arg e | AppUVar(r,vd,args), App(c,hd,[arg]) when c == C.uvarc && matching -> let r_exp = oref C.dummy in - let exp = UVar(r_exp,0,0) in - r @:= UVar(r_exp,0,vd); + let exp = mkUVar r_exp 0 0 in + r @:= mkUVar r_exp 0 vd; unif matching depth adepth exp bdepth hd e && let args = list_to_lp_list (C.mkinterval 0 vd 0 @ args) in unif matching depth adepth args bdepth arg e @@ -1442,7 +1451,7 @@ let rec unif matching depth adepth a bdepth b e = | _, Arg (i,args) -> let v = fst (make_lambdas adepth args) in [%spy "assign" (fun fmt _ -> Fmt.fprintf fmt "%a := %a" - (uppterm depth [] bdepth e) (Arg(i,0)) + (uppterm depth [] bdepth e) (mkArg i 0) (uppterm depth [] bdepth e) v) ()]; e.(i) <- v; [%spy "assign" (ppterm depth [] adepth empty_env) (e.(i))]; @@ -1452,14 +1461,14 @@ let rec unif matching depth adepth a bdepth b e = | _, UVar (r,origdepth,args) when args > 0 -> let v = fst (make_lambdas origdepth args) in [%spy "assign" (fun fmt _ -> Fmt.fprintf fmt "%a := %a" - (uppterm depth [] bdepth e) (UVar(r,origdepth,0)) + (uppterm depth [] bdepth e) (mkUVar r origdepth 0) (uppterm depth [] bdepth e) v) ()]; r @:= v; unif matching depth adepth a bdepth b e | UVar (r,origdepth,args), _ when args > 0 -> let v = fst (make_lambdas origdepth args) in [%spy "assign" (fun fmt _ -> Fmt.fprintf fmt "%a := %a" - (uppterm depth [] adepth e) (UVar(r,origdepth,0)) + (uppterm depth [] adepth e) (mkUVar r origdepth 0) (uppterm depth [] adepth e) v) ()]; r @:= v; unif matching depth adepth a bdepth b e @@ -1469,12 +1478,12 @@ let rec unif matching depth adepth a bdepth b e = let is_llam, args = is_llam adepth args adepth bdepth depth false e in if is_llam then let r = oref C.dummy in - e.(i) <- UVar(r,adepth,0); + e.(i) <- mkUVar r adepth 0; bind r adepth args adepth depth delta bdepth false other e else if !delay_hard_unif_problems then begin Fmt.fprintf Fmt.std_formatter "HO unification delayed: %a = %a\n%!" (uppterm depth [] adepth empty_env) a (uppterm depth [] bdepth e) b ; let r = oref C.dummy in - e.(i) <- UVar(r,adepth,0); + e.(i) <- mkUVar r adepth 0; let kind = Unification {adepth = adepth+depth; env = e; bdepth = bdepth+depth; a; b; matching} in let blockers = match is_flex (adepth+depth) other with @@ -1536,25 +1545,25 @@ let rec unif matching depth adepth a bdepth b e = (* eta *) | Lam t, Const c -> let extra = mkConst (bdepth+depth) in - let eta = App(c,extra,[]) in + let eta = mkApp c extra [] in unif matching (depth+1) adepth t bdepth eta e | Const c, Lam t -> let extra = mkConst (adepth+depth) in - let eta = App(c,extra,[]) in + let eta = mkApp c extra [] in unif matching (depth+1) adepth eta bdepth t e | Lam t, App (c,x,xs) -> let extra = mkConst (bdepth+depth) in let motion = move ~adepth ~from:(bdepth+depth) ~to_:(bdepth+depth+1) e in let x = motion x in let xs = List.map motion xs @ [extra] in - let eta = App(c,x,xs) in + let eta = mkApp c x xs in unif matching (depth+1) adepth t bdepth eta e | App (c,x,xs), Lam t -> let extra = mkConst (adepth+depth) in let motion = hmove ~from:(bdepth+depth) ~to_:(bdepth+depth+1) in let x = motion x in let xs = List.map motion xs @ [extra] in - let eta = App(c,x,xs) in + let eta = mkApp c x xs in unif matching (depth+1) adepth eta bdepth t e | _ -> false @@ -1591,9 +1600,9 @@ let rec deref_head ~depth = function let full_deref ~adepth env ~depth t = let rec deref d = function | Const _ as x -> x - | Lam r -> Lam (deref (d+1) r) - | App (n,x,xs) -> App(n, deref d x, List.map (deref d) xs) - | Cons(hd,tl) -> Cons(deref d hd, deref d tl) + | Lam r -> mkLam (deref (d+1) r) + | App (n,x,xs) -> mkApp n (deref d x) (List.map (deref d) xs) + | Cons(hd,tl) -> mkCons (deref d hd) (deref d tl) | Nil as x -> x | Discard as x -> x | Arg (i,ano) when env.(i) != C.dummy -> @@ -1601,14 +1610,14 @@ let full_deref ~adepth env ~depth t = | Arg _ as x -> x | AppArg (i,args) when env.(i) != C.dummy -> deref d (deref_appuv ~from:adepth ~to_:d args env.(i)) - | AppArg (i,args) -> AppArg (i, List.map (deref d) args) + | AppArg (i,args) -> Term.mkAppArg i (List.map (deref d) args) | UVar (r,lvl,ano) when !!r != C.dummy -> deref d (deref_uv ~from:lvl ~to_:d ano !!r) | UVar _ as x -> x | AppUVar (r,lvl,args) when !!r != C.dummy -> deref d (deref_appuv ~from:lvl ~to_:d args !!r) - | AppUVar (r,lvl,args) -> AppUVar (r,lvl,List.map (deref d) args) - | Builtin(c,xs) -> Builtin(c,List.map (deref d) xs) + | AppUVar (r,lvl,args) -> mkAppUVar r lvl (List.map (deref d) args) + | Builtin(c,xs) -> mkBuiltin c (List.map (deref d) xs) | CData _ as x -> x in deref depth t @@ -1617,14 +1626,14 @@ type assignment = uvar_body * int * term let expand_uv r ~lvl ~ano = let args = C.mkinterval 0 (lvl+ano) 0 in - if lvl = 0 then AppUVar(r,lvl,args), None else + if lvl = 0 then Term.mkAppUVar r lvl args, None else let r1 = oref C.dummy in - let t = AppUVar(r1,0,args) in + let t = Term.mkAppUVar r1 0 args in let assignment = mknLam ano t in t, Some (r,lvl,assignment) let expand_uv ~depth r ~lvl ~ano = [%spy "expand-uv-in" (fun fmt t -> - Fmt.fprintf fmt "%a" (uppterm depth [] 0 empty_env) t) (UVar(r,lvl,ano))]; + Fmt.fprintf fmt "%a" (uppterm depth [] 0 empty_env) t) (mkUVar r lvl ano)]; let t, ass as rc = expand_uv r ~lvl ~ano in [%spy "expand-uv-out" (fun fmt t -> Fmt.fprintf fmt "%a" (uppterm depth [] 0 empty_env) t) t]; @@ -1632,22 +1641,22 @@ let expand_uv ~depth r ~lvl ~ano = | None -> Fmt.fprintf fmt "no assignment" | Some (_,_,t) -> Fmt.fprintf fmt "%a := %a" - (uppterm depth [] 0 empty_env) (UVar(r,lvl,ano)) + (uppterm depth [] 0 empty_env) (mkUVar r lvl ano) (uppterm lvl [] 0 empty_env) t) ass]; rc let expand_appuv r ~lvl ~args = - if lvl = 0 then AppUVar(r,lvl,args), None else + if lvl = 0 then Term.mkAppUVar r lvl args, None else let args_lvl = C.mkinterval 0 lvl 0 in let r1 = oref C.dummy in - let t = AppUVar(r1,0,args_lvl @ args) in + let t = Term.mkAppUVar r1 0 (args_lvl @ args) in let nargs = List.length args in let assignment = - mknLam nargs (AppUVar(r1,0,args_lvl @ C.mkinterval lvl nargs 0)) in + mknLam nargs (Term.mkAppUVar r1 0 (args_lvl @ C.mkinterval lvl nargs 0)) in t, Some (r,lvl,assignment) let expand_appuv ~depth r ~lvl ~args = [%spy "expand-appuv-in" (fun fmt t -> - Fmt.fprintf fmt "%a" (uppterm depth [] 0 empty_env) t) (AppUVar(r,lvl,args))]; + Fmt.fprintf fmt "%a" (uppterm depth [] 0 empty_env) t) (Term.mkAppUVar r lvl args)]; let t, ass as rc = expand_appuv r ~lvl ~args in [%spy "expand-appuv-out" (fun fmt t -> Fmt.fprintf fmt "%a" (uppterm depth [] 0 empty_env) t) t]; @@ -1655,7 +1664,7 @@ let expand_appuv ~depth r ~lvl ~args = | None -> Fmt.fprintf fmt "no assignment" | Some (_,_,t) -> Fmt.fprintf fmt "%a := %a" - (uppterm depth [] 0 empty_env) (AppUVar(r,lvl,args)) + (uppterm depth [] 0 empty_env) (Term.mkAppUVar r lvl args) (uppterm lvl [] 0 empty_env) t) ass]; rc @@ -1666,19 +1675,19 @@ let shift_bound_vars ~depth ~to_ t = else n + to_ - depth in let rec shift d = function | Const n as x -> let m = shift_db d n in if m = n then x else mkConst m - | Lam r -> Lam (shift (d+1) r) + | Lam r -> mkLam (shift (d+1) r) | App (n,x,xs) -> - App(shift_db d n, shift d x, List.map (shift d) xs) - | Cons(hd,tl) -> Cons(shift d hd, shift d tl) + mkApp (shift_db d n) (shift d x) (List.map (shift d) xs) + | Cons(hd,tl) -> mkCons (shift d hd) (shift d tl) | Nil as x -> x | Discard as x -> x | Arg _ as x -> x - | AppArg (i,args) -> AppArg (i, List.map (shift d) args) + | AppArg (i,args) -> Term.mkAppArg i (List.map (shift d) args) | (UVar (r,_,_) | AppUVar(r,_,_)) when !!r != C.dummy -> anomaly "shift_bound_vars: non-derefd term" | UVar _ as x -> x - | AppUVar (r,lvl,args) -> AppUVar (r,lvl,List.map (shift d) args) - | Builtin(c,xs) -> Builtin(c,List.map (shift d) xs) + | AppUVar (r,lvl,args) -> mkAppUVar r lvl (List.map (shift d) args) + | Builtin(c,xs) -> mkBuiltin c (List.map (shift d) xs) | CData _ as x -> x in if depth = to_ then t else shift depth t @@ -1691,19 +1700,19 @@ let subtract_to_consts ~amount ~depth t = else n - amount in let rec shift d = function | Const n as x -> let m = shift_db d n in if m = n then x else mkConst m - | Lam r -> Lam (shift (d+1) r) + | Lam r -> mkLam (shift (d+1) r) | App (n,x,xs) -> - App(shift_db d n, shift d x, List.map (shift d) xs) - | Cons(hd,tl) -> Cons(shift d hd, shift d tl) + mkApp (shift_db d n) (shift d x) (List.map (shift d) xs) + | Cons(hd,tl) -> mkCons (shift d hd) (shift d tl) | Nil as x -> x | Discard as x -> x | Arg _ as x -> x - | AppArg (i,args) -> AppArg (i, List.map (shift d) args) + | AppArg (i,args) -> Term.mkAppArg i (List.map (shift d) args) | (UVar (r,_,_) | AppUVar(r,_,_)) when !!r != C.dummy -> anomaly "subtract_to_consts: non-derefd term" | (UVar _ | AppUVar _) -> error "The term cannot be put in the desired context (leftover uvar)" - | Builtin(c,xs) -> Builtin(c,List.map (shift d) xs) + | Builtin(c,xs) -> mkBuiltin c (List.map (shift d) xs) | CData _ as x -> x in if amount = 0 then t else shift 0 t @@ -1846,7 +1855,7 @@ let hash_arg_list goal hd ~depth args mode spec = (if goal then "goal" else "clause") (dec_to_bin2 h) (pplist ~boxed:true (uppterm depth [] 0 empty_env) " ")) - (Const hd :: args)]; + (mkConst hd :: args)]; h let hash_clause_arg_list = hash_arg_list false @@ -2040,29 +2049,27 @@ let close_with_pis depth vars t = | Const c -> mkConst (fix_const c) | Arg (i,argsno) -> (match C.mkinterval (depth+vars) argsno 0 with - | [] -> Const(i+depth) - | [x] -> App(i+depth,x,[]) - | x::xs -> App(i+depth,x,xs)) + | [] -> mkConst (i+depth) + | x::xs -> mkApp (i+depth) x xs) | AppArg (i,args) -> (match List.map aux args with | [] -> anomaly "AppArg to 0 args" - | [x] -> App(i+depth,x,[]) - | x::xs -> App(i+depth,x,xs)) - | App(c,x,xs) -> App(fix_const c,aux x,List.map aux xs) - | Builtin(c,xs) -> Builtin(c,List.map aux xs) + | x::xs -> mkApp (i+depth) x xs) + | App(c,x,xs) -> mkApp (fix_const c) (aux x) (List.map aux xs) + | Builtin(c,xs) -> mkBuiltin c (List.map aux xs) | UVar(_,_,_) as orig -> (* TODO: quick hack here, but it does not work for AppUVar *) hmove ~from:depth ~to_:(depth+vars) orig | AppUVar(r,vardepth,args) -> assert false (* TODO, essentially almost copy the code from move delta < 0 *) - | Cons(hd,tl) -> Cons(aux hd, aux tl) + | Cons(hd,tl) -> mkCons (aux hd) (aux tl) | Nil as x -> x | Discard as x -> x - | Lam t -> Lam (aux t) + | Lam t -> mkLam (aux t) | CData _ as x -> x in let rec add_pis n t = - if n = 0 then t else App(C.pic,Lam (add_pis (n-1) t),[]) in + if n = 0 then t else mkApp C.pic (mkLam (add_pis (n-1) t)) [] in add_pis vars (aux t) let local_prog { src } = src @@ -2095,15 +2102,15 @@ let rec term_map m = function | Const x when List.mem_assoc x m -> mkConst (List.assoc x m) | Const _ as x -> x | App(c,x,xs) when List.mem_assoc c m -> - App(List.assoc c m,term_map m x, smart_map (term_map m) xs) - | App(c,x,xs) -> App(c,term_map m x, smart_map (term_map m ) xs) - | Lam x -> Lam (term_map m x) + mkApp (List.assoc c m) (term_map m x) (smart_map (term_map m) xs) + | App(c,x,xs) -> mkApp c (term_map m x) (smart_map (term_map m ) xs) + | Lam x -> mkLam (term_map m x) | UVar _ as x -> x - | AppUVar(r,lvl,xs) -> AppUVar(r,lvl,smart_map (term_map m) xs) + | AppUVar(r,lvl,xs) -> mkAppUVar r lvl (smart_map (term_map m) xs) | Arg _ as x -> x - | AppArg(i,xs) -> AppArg(i,smart_map (term_map m) xs) - | Builtin(c,xs) -> Builtin(c,smart_map (term_map m) xs) - | Cons(hd,tl) -> Cons(term_map m hd, term_map m tl) + | AppArg(i,xs) -> Term.mkAppArg i (smart_map (term_map m) xs) + | Builtin(c,xs) -> mkBuiltin c (smart_map (term_map m) xs) + | Cons(hd,tl) -> mkCons (term_map m hd) (term_map m tl) | Nil as x -> x | Discard as x -> x | CData _ as x -> x @@ -2174,12 +2181,12 @@ let rec claux1 ?loc get_mode vars depth hyps ts lts lcs t = List.rev (List.filter (function (Arg _) -> true | _ -> false) ts) in let cst = match args with - [] -> Const (depth+lcs) - | hd::rest -> App (depth+lcs,hd,rest) in + [] -> mkConst (depth+lcs) + | hd::rest -> mkApp (depth+lcs) hd rest in claux1 ?loc get_mode vars depth hyps (cst::ts) (lts+1) (lcs+1) b | App(c, arg, []) when c == C.pic -> let b = get_lambda_body ~depth:(depth+lts) arg in - claux1 ?loc get_mode (vars+1) depth hyps (Arg(vars,0)::ts) (lts+1) lcs b + claux1 ?loc get_mode (vars+1) depth hyps (mkArg vars 0::ts) (lts+1) lcs b | App(c, _, _) when c == C.andc || c == C.andc2 -> error ?loc "Conjunction in the head of a clause is not supported" | Const _ @@ -2366,21 +2373,21 @@ end = struct (* {{{ *) let n, c = C.fresh () in [%spy "freeze-add" (fun fmt tt -> Fmt.fprintf fmt "%s == %a" (C.show n) (ppterm 0 [] 0 empty_env) tt) - (UVar (r,0,0))]; + (mkUVar r 0 0)]; f := { !f with c2uv = C.Map.add n r !f.c2uv; uv2c = (r,c) :: !f.uv2c }; c in let rec faux d = function | (Const _ | CData _ | Nil | Discard) as x -> x - | Cons(hd,tl) -> Cons(faux d hd, faux d tl) - | App(c,x,xs) -> App(c,faux d x, List.map (faux d) xs) - | Builtin(c,args) -> Builtin(c,List.map (faux d) args) + | Cons(hd,tl) -> mkCons (faux d hd) (faux d tl) + | App(c,x,xs) -> mkApp c (faux d x) (List.map (faux d) xs) + | Builtin(c,args) -> mkBuiltin c (List.map (faux d) args) | (Arg _ | AppArg _) -> error "only heap terms can be frozen" - | Lam t -> Lam (faux (d+1) t) + | Lam t -> mkLam (faux (d+1) t) (* freeze *) | AppUVar(r,0,args) when !!r == C.dummy -> let args = List.map (faux d) args in - App(C.uvarc, freeze_uv r, [list_to_lp_list args]) + mkApp C.uvarc (freeze_uv r) [list_to_lp_list args] (* expansion *) | UVar(r,lvl,ano) when !!r == C.dummy -> faux d (log_assignment(expand_uv ~depth:d r ~lvl ~ano)) @@ -2421,25 +2428,25 @@ end = struct (* {{{ *) (uppterm to_ [] 0 empty_env) t) t]; let rec daux d = function | Const c when C.Map.mem c f.c2uv -> - UVar(C.Map.find c f.c2uv,0,0) + mkUVar (C.Map.find c f.c2uv) 0 0 | (Const _ | CData _ | Nil | Discard) as x -> x - | Cons(hd,tl) -> Cons(daux d hd, daux d tl) + | Cons(hd,tl) -> mkCons (daux d hd) (daux d tl) | App(c,Const x,[args]) when c == C.uvarc -> let r = C.Map.find x f.c2uv in let args = lp_list_to_list ~depth:d args in mkAppUVar r 0 (List.map (daux d) args) - | App(c,x,xs) -> App(c,daux d x, List.map (daux d) xs) - | Builtin(c,args) -> Builtin(c,List.map (daux d) args) + | App(c,x,xs) -> mkApp c (daux d x) (List.map (daux d) xs) + | Builtin(c,args) -> mkBuiltin c (List.map (daux d) args) | Arg(i,ano) when env.(i) != C.dummy -> daux d (deref_uv ~from:to_ ~to_:d ano env.(i)) | AppArg (i,args) when env.(i) != C.dummy -> daux d (deref_appuv ~from:to_ ~to_:d args env.(i)) | (Arg(i,_) | AppArg(i,_)) as x -> - env.(i) <- UVar(oref C.dummy, to_, 0); + env.(i) <- mkUVar (oref C.dummy) to_ 0; daux d x - | Lam t -> Lam (daux (d+1) t) + | Lam t -> mkLam (daux (d+1) t) | UVar _ as x -> x - | AppUVar(r,lvl,args) -> AppUVar(r,lvl,List.map (daux d) args) + | AppUVar(r,lvl,args) -> mkAppUVar r lvl (List.map (daux d) args) in daux to_ t @@ -2448,15 +2455,17 @@ end = struct (* {{{ *) let replace_const m t = let rec rcaux = function | Const c as x -> (try mkConst (List.assoc c m) with Not_found -> x) - | Lam t -> Lam (rcaux t) + | Lam t -> mkLam (rcaux t) | App(c,x,xs) -> - App((try List.assoc c m with Not_found -> c), - rcaux x, smart_map rcaux xs) - | Builtin(c,xs) -> Builtin(c,smart_map rcaux xs) - | Cons(hd,tl) -> Cons(rcaux hd, rcaux tl) + mkApp + (try List.assoc c m with Not_found -> c) + (rcaux x) + (smart_map rcaux xs) + | Builtin(c,xs) -> mkBuiltin c (smart_map rcaux xs) + | Cons(hd,tl) -> mkCons (rcaux hd) (rcaux tl) | (CData _ | UVar _ | Nil | Discard) as x -> x | Arg _ | AppArg _ -> assert false - | AppUVar(r,lvl,args) -> AppUVar(r,lvl,smart_map rcaux args) in + | AppUVar(r,lvl,args) -> mkAppUVar r lvl (smart_map rcaux args) in [%spy "alignment-replace-in" (uppterm 0 [] 0 empty_env) t]; let t = rcaux t in [%spy "alignment-replace-out" (uppterm 0 [] 0 empty_env) t]; @@ -2610,7 +2619,7 @@ let mk_out_assign ~depth { Conversion.embed } bname hyps constraints state input | Some _, BuiltInPredicate.Discard -> state, [] (* We could warn that such output was generated without being required *) | Some t, BuiltInPredicate.Keep -> let state, t, extra = embed ~depth hyps constraints state t in - state, extra @ [App(C.eqc, v, [t])] + state, extra @ [mkApp C.eqc v [t]] | None, BuiltInPredicate.Keep -> anomaly ("ffi: " ^ bname ^ ": some output was requested but not produced") @@ -2620,7 +2629,7 @@ let mk_inout_assign ~depth { Conversion.embed } bname hyps constraints state inp | Some _, BuiltInPredicate.NoData -> state, [] (* We could warn that such output was generated without being required *) | Some t, BuiltInPredicate.Data _ -> let state, t, extra = embed ~depth hyps constraints state t in - state, extra @ [App(C.eqc, v, [t])] + state, extra @ [mkApp C.eqc v [t]] | None, BuiltInPredicate.Data _ -> anomaly ("ffi: " ^ bname ^ ": some output was requested but not produced") @@ -2854,7 +2863,7 @@ let try_fire_rule rule (constraints as orig_constraints) = | _ -> error "eigen not resolving to an integer" in let conclusion = Ice.defrost ~maxd:max_depth ~to_:eigen - (App(C.implc,context,[conclusion])) env m in + (mkApp C.implc context [conclusion]) env m in (* TODO: check things make sense in heigen *) let prog = initial_program in [{ cdepth = eigen; prog; context = []; conclusion }] in @@ -3018,7 +3027,7 @@ let make_runtime : ?max_steps: int -> ?delay_outside_fragment: bool -> 'x execut run (depth+1) p f gs next alts lvl | App(c, arg, []) when c == C.sigmac -> let f = get_lambda_body ~depth arg in - let v = UVar(oref C.dummy, depth, 0) in + let v = mkUVar (oref C.dummy) depth 0 in run depth p (subst depth [v] f) gs next alts lvl | UVar ({ contents = g }, from, args) when g != C.dummy -> run depth p (deref_uv ~from ~to_:depth args g) gs next alts lvl